COMMON DERIVATIONS IN LOCALLY DETERMINED NONMONOTONIC RULE SYSTEMS AND THEIR COMPLEXITY By AMY K. C. S. VANDERBILT A DISSERTATION PRESENTED TO THE GRADUATE SCHOOL OF THE UNIVERSITY OF FLORIDA IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF DOCTOR OF PHILOSOPHY UNIVERSITY OF FLORIDA 2000 I dedicate this dissertation to the memory of Sara Davidson Sartain, who put her foot down. Most importantly, I dedicate it to Scott and Sabrina, for whom I would accomplish anything and with whom I could accomplish anything. ACKNOWLEDGMENTS I would like to thank the University of Florida and the Department of Math- ematics for their encouragement and contributions to my education, experience, and funding. Special and heart-felt thanks go to my committee, who from the first day were supportive and helpful above and beyond the call of duty. Thanks to my parents, Ronald and Linda Sartain, without whom I might never have taken my education this far and without whom I might never have gone to conferences! An enormous thanks to my advisor, Dr. Douglas A. Cenzer, who not only put up with me for these years, but encouraged my tenacious approach and worked to help me achieve my goals, both for this dissertation and for the years beyond. Lastly, the greatest thanks go to my husband, Scott, for constant encouragement and support (and chocolate pie!), and to my daughter, Sabrina, who (although not around for the entire undertaking) was there with daily hugs and smiles and reminders of what life is really about. in TABLE OF CONTENTS pa g e ACKNOWLEDGEMENTS iii ABSTRACT vi 1 INTRODUCTION 1 1.1 History 1 1 .2 Motivation 3 1 .3 Preliminary Theorems and Definitions: Nonmonotonic Rule Systems 5 1 .4 Common Derivations in Locally Determined Systems 16 2 THE FINITE CASE 18 2.1 Finite Classical Nonmonotonic Rule Systems 18 2.2 Finite Constructive Nonmonotonic Rule Systems 32 2.3 Characterizing the Set of Extensions 36 3 THE INFINITE CASE 38 3 . 1 Locally Finite Classical Nonmonotonic Rule Systems 38 3 .2 Locally Finite Constructive Nonmonotonic Rule Systems 51 3.3 Characterizing The Set of Extensions 59 4 LOCALLY DETERMINED NONMONOTONIC RULE SYSTEMS 60 4. 1 Locally Determined Nonmonotonic Rule Systems 60 4.2 Common Derivations in Locally Determined Nonmonotonic Rule Systems 67 4.3 Characterizing the Set of Extensions 69 5 COMPUT ABILITY AND COMPLEXITY ISSUES 76 5.1 Finding Extensions with Low Complexity 76 5.2 Computability and Complexity of Common Derivations 82 IV 6 ALTERNATE FORMALISMS OF NONMONOTONIC LOGIC 86 6.1 Default Logic: Preliminary Definitions and Theorems 86 6.2 Equivalence of Default Logic to Nonmonotonic Rule Systems 90 6.3 Previous Results Through the Eyes of Default Logic 91 6.4 Logic Programming: Preliminary Definitions and Theorems 114 6.5 Equivalence of Logic Programming to Nonmonotonic Rule Systems 120 6.6 Previous Results Through the Eyes of Logic Programming 121 7 FUTURE DIRECTIONS 131 REFERENCES 133 BIOGRAPHICAL SKETCH 137 Abstract of Dissertation Presented to the Graduate School of the University of Florida in Partial Fulfillment of the Requirements for the Degree of Doctor of Philosophy COMMON DERIVATIONS IN LOCALLY DETERMINED NONMONOTONIC RULE SYSTEMS AND THEIR COMPLEXITY By Amy K. C. S. Vanderbilt May 2000 Chairman: Douglas Cenzer Major Department: Mathematics Nonmonotonic Rule Systems are a general framework for commonsense rea- soning. U =< U,N > is a nonmonotonic rule system where the universe U is a countable set, such as the set of sentences of some propositional logic; N is a set of rules of inference under which a conclusion from U may be inferred from the pres- ence of premises and the absence of restraints. An extension of U is a set of beliefs concurrent with the rules of inference. If <j> is a formula of the language, appearing in every extension of < U, N >, then <\> has a common derivation d 1 ^ that gener- ates (j) in every extension. Further, every extension of < U, N > is an extension of < U, N U {d l <p} >. These two sets of extensions may be equal, but this is not al- ways true. A constructive view enhances as well as simplifies the results. We explore alternate forms of the common derivation d that ensure certain properties for the re- sulting nonmonotonic rule system < U, N U {d} > . We then introduce the notion of levels and locally determined systems. The previous questions are explored in terms VI of these systems. Computability and complexity issues of the common derivations are considered. Several conditions are detailed, based on the notion of levels, which ensure that a nonmonotonic rule system will have a computable extension. These results are refined to give conditions which ensure the existence of extensions of low complexity (such as exponential time). If U is a recursive nonmonotonic rule system with (effective) levels, there is a 1:1 degree preserving correspondence between the set of extensions of U and the set of paths through a recursive finitely branching (highly recursive) tree. The families of extensions of a nonmonotonic rule system with levels are characterized. We find that for any closed (Ilf) family S of subsets of U having levels, there exists a (recursive) nonmonotonic rule system U with (recursive) levels such that S is the set of extensions of U. vii CHAPTER 1 INTRODUCTION In this chapter, we provide a motivation for the directions of the research as well as necessary background definitions and preliminary theorems. Along with this, we take a short exploration of the history of the subject and of the directions research in the field is presently taking. 1.1 History In mathematics, a conclusion drawn from a set of axioms can also be drawn from any larger set of axioms containing the original set. The deduction remains no matter how the axioms are increased. This is monotonic reasoning in that new information does not affect the conclusions drawn from a set of premises. From the time of Euclid, it has been the nature of this monotonic reasoning that makes math- ematical proofs permanent. Complete proofs of theorems are never later withdrawn due to new information. There is, however, another sort of reasoning that is not monotonic. In this type of reasoning, we deduce a statement based on the absence of any evidence to the contrary. Such a statement is therefore more of a belief than a truth, as we may later come upon new information that contradicts the statement. Statistics is often used as a tool for for deducing provisional beliefs, but not every problem comes with its own set of distributions ready for use. Such deductions may arise in situations where we are made to choose con- cretely between two actions in the absence of complete information. It may be that we cannot wait for the complete information to show itself, or that we have no guar- antee that it will ever show itself. Thus beliefs are often accepted as truth based on a lack of contradicting facts. One of the standard illustrations of this commonsense reasoning is the "Tweety" example. If we see only birds that can fly, then we deduce that birds can fly. If Tweety is a bird, we conclude that Tweety can fly. If we later find that Tweety is a penguin, then we are forced to retract our conclusion that Tweety can fly. We are back to knowing only that Tweety is a bird, specifically a penguin. Every vision of a nonmonotonic logic describing belief will be similar, depend- ing only on our definition of a lack of evidence against a conclusion. McCarthy [1980] was one of several who initiated formalizations of nonmonotonic logic with his concept of Circumscription. At the same time, Reiter [Rei80] created a formalization that he termed Default Logic. Along with these are the Theory of Multiple Believers of Hintikka (1962), the Truth Maintenance Systems of Doyle [Do79], the Autoepistemic Logic of Moore (1985), the Theory of Individual and Common Knowledge and Belief of Halpern and Moses (1984), and Logic Programming with Negation as Failure given by Apt (1988). This is only a partial list. The first journeys into the nonmonotonic aspects of logic can be traced to Reiter's Default Logic [Rei80]. This involved creating a natural extension of classical logic that would easily handle negative information. These nonmonotonic logics share many properties. Several translations be- tween them have been made by Konolige (1988), Gelfond and Przymusihska (1986, 1989), Reinfrank and Dressier (1989), and Marek and Truszczyhski (1989). It should be noted that these translations are primarily for propositional logic. Apt [A90], and Gelfond and Lifschitz [GL88] studied negation as failure in logic programming. It has since been seen that each of these investigations were in a common direction. Relationships were discovered by several, including Marek and Trusczcynski (1989), who explored the precise nature of the connections between Default Logic and Logic Programming. Since then, many aspects of the computability and complexity of the exten- sions of these systems have been explored. Subsequently, algorithms for computing the extensions of any one theory have been created. More importantly, a universal system of nonmonotonic logic called Nonmonotonic Rule Systems was created by Marek, Nerode, and Remmel [MNR90 and MNR92a]. This system has been shown by Marek, Nerode, and Remmel and others to be equivalent to many other systems of nonmonotonic logic including Reiter's Default Logic as well as Logic Programming, and Modal Nonmonotonic Logic. 1.2 Motivation We suppose that we have a sentence (j) appearing in some or all extensions of a nonmonotonic rule system. We want to then construct a single rule that would derive 4> in every extension of the system. The motivation behind this "common derivation" is that it would tell us what is required, in a nutshell, to derive <j> in this system. Nonmonotonic Logic has a place in fields such as medicine and political science where this kind of information would be useful. In the world of medical diagnoses, we imagine that our system involves a universe U of symptoms to be matched with a diagnosis. We would care to know a concise list of what symptoms should be present and, just as importantly, what symptoms should be absent in order to accurately diagnose a condition. My ultimate goal is to manipulate Nonmonotonic Rule Systems to create a mathematical system which would lend itself to applications in political science (and possibly social science as a whole as well as advertising) and explore the subsequent theory of that system. First Order Logic is inherently monotonic. Human reasoning, however, in- volves not only the addition of beliefs, but the retraction of beliefs, based on new information, i.e. it is nonmonotonic. For example, the study of Astronomy led to the retraction of the belief of a geocentric universe. Thus, to formalize human reasoning, a nonmonotonic logic is needed. I propose to consider Political Science as an area of future application. This area is ripe for the use of Nonmonotonic Logic since Political Science studies how groups of people react to a campaign and how they reason who they will vote for. If human reasoning can be formalized, then the reasoning of the electorate can be modeled. Other types of mathematics used to model the electorate in the past include statistics, game theory [Gol94] and measure theory [B90]. Some of these models managed to get as accurate as 84 percent [Gol94], but had to be redone every time a subset of the electorate changed its mind (which was often!). Secondly, the accuracy of the model was only known after the election was already over. These two properties made the models unreliable and expensive. The problem: these types of mathematics are monotonic, so the conclusions they reach cannot be retracted upon receipt of new information. We imagine that we create one nonmonotonic rule system per category of voters and we consider the extensions of each theory or system. We would like all the extensions for a category to contain some conclusion such as, "I will vote for candidate A." For this reason, we take great interest not only in the intersections of extensions, but also in the process of deduction used to create those extensions. It is for this reason that we explore the concept of a common derivation for a conclusion that appears in some or all extensions. Having one rule that derives the conclusion "I will vote for candidate A" in each extension allows us to see exactly what must be concluded previously and what must not have been concluded in order to allow the derivation to apply. 1.3 Preliminary Theorems and Definitions: Nonmonotonic Rule Systems The following background is taken from Marek, Nerode, and Remmel's series of papers [MNR90] and [MNR92a]. Here we introduce the notion of a nonmonotonic formal system < U, N >. Definition 1.3.1 A NONMONOTONIC RULE OF INFERENCE is a triple <P,R,d>>, where P = {a>i,...,a n }, and R = {/?i,...,/? m } are finite lists of objects from U and 4> G U. Each such rule is written in the form r = a\,...,a n : /3 1} ...,/3 m /0. Here {a\,...,a n } are called the PREMISES of the rule r, {/?i,...,/? m } are called the RE- STRAINTS of the rule r, and cln(r) = c{r) = </> is the CONCLUSION ofr. Either P or R or both may be empty. If R is empty, then the rule is monotonic. In the case that both P and R are empty, we call the rule r an axiom. For a set A of rules, let c(A) = {c(r)\r e A}. A NONMONOTONIC FORMAL SYSTEM is a pair <U,N>, where U is a nonempty set and N is a set of nonmonotonic rules. Each monotonic formal system can be identified with the nonmonotonic formal system in which every monotonic rule is given an empty set of restraints. The standard example for U will be the set Sent(V) of propositional sentences on a finite or countable set of propositional variables (or atoms). Here we will frequently assume that the standard propositional rules of deduction are implicitly included as monotonic rules in any nonmonotonic rule system with universe U. In the constructive case, a proper subset of these rules are assumed. Now, if < U, N > is a nonmonotonic rule system, and 5 is a set of formulas of the language, call a rule r <E N GENERATING FOR THE CONTEXT S if the premises of r are in S, and no element of the restraints is in S. Let GD(N, S) be the set of all rules in N that generate for the context S. 6 A subset S C U is called DEDUCTIVELY CLOSED if for every rule r £ N, we have that if all premises {ai,...,a n } are in S and all restraints {/?i,..., /3 m } are not in S then the conclusion belongs to 5. In nonmonotonic rule systems, deductively closed sets are not generally closed under arbitrary intersections as in the monotone case. But deductively closed sets are closed under intersections of descending chains. Since U is deductively closed, by the Kuratowski-Zorn Lemma, any / C U is contained in at least one minimal deductively closed set. The intersection of all the deductively closed sets containing / is called the set of SECURED CONSEQUENCES of /. This set is also the intersection of all minimal deductively closed sets containing /. Deductively closed sets are thought of as representing possible "points of view." the intersection of all deductively closed sets containing / represents the common information present in all such "points of view" containing /. Example 1.3.1 Let U = {a,b,c}. (a) Consider U with Ni = {: /a; a : — >6/6} . There is only one minimal deductively closed set S — {a, b}. Then S is the set of secured consequences of <U,N X >. (b) Consider U with N 2 = {: / o; a : b/c; a : c/b). Then there are two minimal deductively closed sets, S x = {a,b} and S 2 = {a,c}. The singleton set {a} is the set of secured consequences of < U, N 2 > . Part (b) of this example shows that the set of all secured consequences is not, in general, deductively closed in the nonmonotone case. Note that if we implicitly assume the rules of propositional logic we define Cn(S) to be the closure of the set S under these implicit monotonic rules Given a set S and an / C U, and 5-DERIVATION of </> from / in the system < U, N > is a finite sequence < 0!,...,^ > such that <f> k = cf> and, for all i < k, each 0i is in /, or is an axiom, or is the conclusion of a rule r e N such that all the premises of r are included in {(fii,..., <j>i-\) and all restraints of r are in U — S. An S- CONSEQUENCE of I is an element of U occurring in some 5-deduction from /. Let Cs{I) be the set of all S-consequences of / in < U, N >. I is a subset of Cs(I). Note that S enters solely as a restraint on the use of the rules imposed by the restraints in the rules. A single restraint in a rule in N may be in S and therefore prevent the rule from ever being applied in an 5-deduction from /, even though all the premises of that rule occur earlier in the deduction. Thus, S contributes no members directly to Cs(I), although members of S may turn up in Cs{I) by an application of a rule which happens to have its conclusion in S. For a fixed S, the operator Cs(*) is monotonic. That is, if IC J, then C S (I) C C S (J). Also, C S (C S {I)) = C S (I). Generally, Cs(I) is not deductively closed in < U, N >. It is possible that all the premises of a rule be in Cs(I), the restraints of that rule are outside of Cs(I), but a restraint of that rule be in 5, preventing the conclusion from being put into Cs(I). Example 1.3.2 Let U = {a,b,c},N = {: /a;a: b/c}, and S = {b}. Then, C s (0) ■ {a} is not deductively closed. However, we do get the following result: Theorem 1.3.2 (MNR90) If S C C S {I) then C S (I) is deductively closed. We say that S C U is an EXTENSION of / if C S (I) = S. S is an extension of / if two things happen. First, every element of S is deducible from /, that is, S C C S (I) (this is the analogue of the adequacy property in logical calculi). Second, the converse holds: all the 5-consequences of / belong to S (this is the analogue of completeness). In purely monotonic rule systems, extensions usually refer to larger theories (under inclusion). This is definitely not the meaning of extension for nonmonotonic rule systems. In fact, it will be seen that for any two extensions A and B of a nonmonotonic rule system, it is never the case that A C B. An important family in propositional logic is the set of complete consistent extensions, CCE(T), of a theory T. Any such family can be obtained as the set of extensions of a nonmonotonic rule system. We obtain this system by taking the monotonic rules as restraint-free nonmonotonic rules and adding rules of the form : (j>/-<<j) and : ->0/</>, for each sentence 4> (to secure completeness). The notion of an extension is related to that of a minimal deductively closed set. Theorem 1.3.3 (MNR90) // S is an extension of I, then: (1) S is a minimal deductively closed superset of I. (2) For every V such that I C /' C S, Cs(I') = S. Example 1.3.3 Let a, b, and c be atoms in the language L and let U = {a,b,c} and iV = {:{a}/6,:{c}/6,:{a}/c,:{c}/a}. Then the nonmonotonic rule system < U,N > has two extensions: 5i = {6,c} and Moreover, we find that S 2 = {b,a}. GD(N,S 1 ) = {:{a}/b,:{a}/c} and GD(N,S 2 ) = {:{c}/b,:{c}/a}. Now, we may well-order the rules of a nonmonotonic rule system < U, N > by some well-ordering < We may then define AD^. to be the set of all rules in TV which are applied when the well-ordering is used to close under the set of rules. This is done in the following way: we define an ordinal tfc. For every e < 77^ we define a set of rules AD £ and a rule r e . If the sets AD £ , e < a, have been defined but 77^ has not been defined, then a rule r is applicable at stage a if the following two conditions hold: (*)c(U t<a AD t )\-P(r) ( b ) c(U £ <a AD e ) \f (3, for every € R(r). (1) If there is no applicable rule r £ N\ [) £<a AD £ , then r^ = a and AD Q = (2) Otherwise, define r Q to be the ^-least applicable rule r e N\ \J £<Q AD e and set AD a = (|J e<a AD,) U{r a }. (3) Put AD± = U £< ^ AD S . Intuitively, we begin with the empty set of formulas and apply the rules of TV in their order. Each time we apply only the ordering-least rule which can be applied. At some point (since the ordinal is well-defined [MT93a]) there will be no available rules that may be applied. At this point, AD± is the set of all rules applied and r^ is the number of steps needed to reach this stopping point. Then, let T± be c(AD^). This is the theory GENERATED BY < Then, GD(N,T^) CAD± so that c(GD(N,T±))CT±. 10 Now, if X is a well-ordering of the rules and for every /? in R(AD^), (5 £ c(AD^) then T-< is an extension of < U, N >. That is, if AD± = GD(N,T±), then T± = c(AD^) is an extension of < U, N >. More precisely, if 71< = c(GD(N,T±)), then T< is an extension of < U, N > . We now have that (a) [MT93a] If S is an extension of < U, N > then there is some well-ordering ^ of the rules in N such that S = c(AD±) = c{GD{N,S)). And, (b) US = T^ = c(AD^) = c(GD(N,S)) for some well-ordering <, then S is an extension of < U, N > . Thus, S is an extension of < U, N > if and only if S = c(GD(N, S)). It is important to note that a well-ordering may not give rise to an extension. The new rule r Q may have a conclusion that contradicts the restraint of a previously applied rule. Then, T-< is not an extension. Consider the following example: Example 1.3.4 Let < U,N > be the nonmonotonic rule system where U = {a,b} and N = {: {a}/b; b : /a}. Then rule r x is applicable at stage one. At stage two, rule r 2 is applicable; however, the conclusion of r 2 violates the restraint of r l . Thus, this system has no extensions. Thus, we must concede that if c((J £<Q AD e ) h (3, where /? € R(r) for some rule r € [j e<a AD e , then the well-ordering does not define an extension. 11 Let £(< U,N >) be the set of all extensions of the nonmonotonic rule system <U,N >. Call two nonmonotonic rule systems <U\,Ni> and < U 2 , N 2 > EQUIV- ALENT, written < Ui,N\ >=< U 2 , N 2 >, if they have exactly the same extensions, i.e., if £{< U u Ni >) = £(< U 2 ,N 2 >) [MT93a]. Example 1.3.5 Let < U,N > be a nonmonotonic rule system where U = {a, b}, and N\ = {: /a;a : /b}. Then consider the nonmonotonic rule system < U, N 2 > where N 2 = {: /b;b : /a). These two theories are equivalent as they each have the same single extension S = {a,b}. Theorem 1.3.4 (MT93) A nonmonotonic rule system <U,N > has an inconsis- tent extension if and only if Sent(L) is an extension and < U,N > has no other extensions. Theorem 1.3.5 (MNR90) The set of extensions of a nonmonotonic rule system forms an antichain. That is, if S\ , S 2 are extensions of a nonmonotonic rule system <U,N > and Si C S 2 , then S x = S 2 . Though this is a widely known fact about all forms of nonmonotonic logic, this is an important concept for the characterization of the family of extensions of a nonmonotonic rule system The natural question here is under what conditions is an antichain the set of extensions of a nonmonotonic rule system? Consider the following example: Example 1.3.6 Considering the monotonic theory T = Cn(a — ► b) and the set V = {a, 6} of atoms. The set of complete consistent extensions of this monotonic 12 theory can be seen as the set of extensions of the nonmonotonic rule system < V, N > where N = {: ->a/a; : a/->a; : — >6/6; : b/-<b; a : /b}. This system has three extensions: S 1 = Gn({a,6}), S 2 = Cn({^a,b}), and S 3 = Cn({^a,^b}). It will not always be so easy to construct a nonmonotonic rule system whose extensions are exactly what we want them to be. We address this in detatil in subsequent chapters. Next we need to define the notions of recursive and highly recursive non- monotonic rule systems < U,N >. Without loss of generality, we may assume that U C u and we will identify a rule r = ai,...,a n : /? lv ..,/? m /0 in N with its code c(r) =< k,l,<j>> where D k = {a u ...,a n } and D t = {/?i,...,/J m }. In this way, we can think of iV as a subset of a;. We say that a nonmonotonic rule system < U, N > is RECURSIVE if both U and N are recursive subsets of w. To define the notion of a highly recursive nonmonotonic rule system < U, N >, we must first introduce the concept of a PROOF SCHEME for in < U, N >. A proof scheme for is a finite sequence p =<< <j> Q ,ro,can(G ) >,...,< ^m,?"m,con(G m ) >> such that <f> m = <f> and (1) If m = then: (a) O is an axiom (that is, there exists a rule r g N,r =: M>), r o = r > and G = or (b) is a conclusion of a rule r =: 0t,..., /3 T , r = r, and Go = {A, •.,&}• (2) m > 0, << o ,r o ,can(Go) >,...,< <^ m _i,r m _ 1 ,can(G m _ 1 ) >> is a proof scheme of length m and <j> m is a conclusion of r = ^ io ,...,^ : p u ..., /3 r /(t) m where to,..., i s <m,r m = r, and G m = G m _i U {A,..., /? r }. 13 The formula m is called the CONCLUSION of the proof scheme p and denoted by cln(p), the set G m is called the SUPPORT of p and is denoted by supp(p). The idea behind this concept is this: any 5-derivation, p, in the system U =< U,N >, uses some negative information about S to ensure that the restraints of rules that were used are outside of S. But this negative information is finite, that is, it involves a finte subset of the complement of 5, such that as long as G fl S\ = 0, p is an Si-derivation as well. In the notion of proof scheme we capture this finitary character of the 5-derivation. A proof scheme with the conclusion </> may include a number of rules that are irrelevant to the enterprise of deriving <f>. There is a natural preordering on proof schemes. Namely, we say that p < p\ if every rule appearing in p also appears in p x . The relation is not a partial ordering, and it is not a partial ordering if we restrict ourselves to proof schemes with a fixed conclusion </>. Yet it is a well-founded relation, namely, for every proof scheme p there exists a MINIMAL PROOF SCHEME p\ <p [e.g. q is minimal if for every p 2 , if p<i -< q, then q -< p 2 ] moreover, we can, if desired, require the conclusion of p x to be the same as that of p. We also set p = pi equivalent to p -< p x A p\ < p and see that = is an equivalence relation and that its equivalence classes are finite. We say that the nonmonotonic rule system < U, N > is LOCALLY FINITE if for every $€U there are finitely many -<-minimal proof schemes with conclusion <j>. This concept is motivated by the fact that, for locally finite systems, for every there is a finite set, Dr^, of derivations such that all the derivations of are inessential extensions of derivations in Dr^. That is, if p is a derivation of 0, then there is a derivation p x e Dr^ such that p x -< p. Finally, we say that the system < U, N > is HIGHLY RECURSIVE if it is recursive, locally finite, and the map — ► can{Dr^) is partial recursive. That is, there exists an effective procedure which, given any 14 4> 6 U, produces a canonical index of the set of all -<-minimal proof schemes with conclusion (j>. We let £(< U, N >) denote the set of extensions of the system. For a nonmonotonic rule system < U, N >, define a rule r to be RESTRAINT- FREE if its set of restraints is empty. Define a sentence <\> G U to be TERMINALLY RESTRAINT-FREE if the last rule in each of its minimal proof schemes is restraint free. Define a subset A of U to be terminally restraint-free if every sentence <j) G A is terminally restraint free. Definition 1.3.6 For a nonmonotonic rule system < U,N >, define a sentence 4> G U to be PREMISE-FREE if each of its minimal proof schemes has length one. Define a subset A of U to be premise-free if every sentence (j) G A is premise-free. Definition 1.3.7 For a nonmonotonic rule system < U,N >, define a rule r to be NORMAL if the set of restraints consists only of the negation of the conclusion. Define a sentence (j> G U to be TERMINALLY NORMAL if the last rule in each of its minimal proof schemes is normal. Define a subset A of U to be terminally normal if every sentence (f> G A is terminally normal. To consider the relationship between sets of extensions and trees, we will need the following background, as given by Cenzer and Remmel [CR99]. Let u = {0,1,2,...} denote the set of natural numbers and let <,>: u x w — > u be some fixed one-to-one and onto recursive pairing function such that the projection functions 7Ti and n 2 defined by 7T!(< x,y >) = x and 7r 2 (< x,y >) = y are also recursive. We extend our pairing function to code n-tuples for n > 2 by the usual inductive definition, that is < Xi,...,x„ >=< x x , < x 2 ,...,x n » for n i 2. We let a; <tJ denote the set of all finite sequences from u and 2 <UJ denote the set of all finite sequences of 0's and l's. Given a =< a>i,...,a n > and =< (5 U ... , (3 k > in uj <uj we write a Q (5 if o: is an initial segment of /?. Now we can identify a sequence 15 a =< a lr .., a n > with its code c(a) =< n, < tti,..., a n >> in u>. We let be the code of the empty sequence 0. Thus, when we say a set 5 C u> <u) is recursive or recursively enumerable, we mean the set {c(oj)|o; G S} is recursive or recursively enumerable. A TREE T is a nonempty subset of cj <w such that T is closed under initial segments. A function / : u — ► w is an infinite PATH through T if for all n, < /(0),..., f(n) >G T. We let P(T) denote the set of all paths through T. A set A of functions is a II ! class if there is a recursive predicate R such that A — {/ G w w |(Vn), R(< /(0),...,/(n) >)}. A n°i class is RECURSIVELY BOUNDED if there is a recursive function g : u — ► u such that V/ G A, Vn, /(n) < g(n). A is a U°i class, if an only if A = P(T) for some recursive tree T. We say that a tree T is HIGHLY RECURSIVE if T is a recursive, finitely branching tree such that there is a recursive procedure which, given a =< a\, ...,a n > in T produces a canonical index of the set of immediate sucessors of a in T, that is, produces a canonical index of {(3 =< <*i,..., a n , k > \fi GT}. Here we say the canonical index, can(X) of the finite set X = {xi <...< x n ) C u is 2 Xl + ...+2 Xn and the canonical index of the empty set is 0. We let D k denote the finite set whose canonical index is k, that is can(D k ) = k. It is then the case that if A is a recursively bounded n°! class, then A - P(T) for some highly recursive tree T. We note that if T is a binary tree, then the set of paths through T is a collection of {0, 1} -valued functions and by identifying each function / G P(T) with the set A f = {x\f(x) = 1} of which / is the characteristic function, we can think of the set of paths through T as a n°! class of sets. We then have the following theorem: Theorem 1.3.8 (MNR92a) Given a highly recursive nonmonotonic rule system < U,N >, there is a highly recursive binary tree T such that there is an effective one- to-one degree-preserving correspondence between the set of extensions of the system and the set P(T) of infinite paths through T. 16 A bit more is required for the reverse implication, but it may be shown in the following sense: Theorem 1.3.9 (MNR92a) For any recursive binary tree, there is a highly re- cursive nonmonotonic rule system such that there is an effective one-to-one degree- preserving correspondence between the set of extensions of the system and the set P{T) of infinite paths through T. The significance of these results is that we can apply recursive IT ! classes to obtain numerous corollaries [MNR92a, CR98]. Corollary 1.3.10 (CR99) Let S = (U,N) be a highly recursive nonmonotonic rule system such that £(S) ^ 0. Then (i) If S has only finitely many extensions, then every extension E of S is recursive. A new representation result is given in chapter four for locally determined nonmonotonic rule systems. 1.4 Common Derivations and Locally Determined Systems In the second chapter we consider the finite case in which a nonmonotonic rule system has a finite language and/or finitely many extensions. Within this chapter we consider various forms of the common derivation of a sentence appearing in all or some of the extensions of a nonmonotonic rule system. Certain forms of the common derivation are explored not only in the classical sense but also using a constructive view. The infinite case is explored in the third chapter in which we have an infinite number of extensions and/or an infinite language. Within this chapter, as in the second, we consider various forms of the common derivation for a sentence appearing in all or some of the extensions of a nonmonotonic rule system. Each of these is 17 explored in the classical sense as well as with a constructive view. We consider the problem of characterizing the set of extensions of a locally finite nonmonotonic rule system. Locally determined nonmonotonic rule systems are introduced in the fourth chapter. When considering nonmonotonic rule systems with an infinite language, a problem arises in being able to determine at what stage we are sure to either have concluded <j> or (in the case of restraints) not have concluded 4> for some 4> E U. To solve this problem, the notion of "levels" was devised. Intuitively, we require that for each i (as we take U to be enumerated {fa, fa, •••}), there is a fixed n x such that the inclusion or exclusion of fa is determined by the n^-th stage. Hence the term "locally determined" is used. This concept allows us to extend results from the infinite case. The set of extensions of a locally determined nonmonotonic rule system is characterized in general and in the effective setting. In the fifth chapter, we consider the complexity of the sets of extensions and explore the comparative complexity of the common derivations themselves. Within these systems we explore both the finite and infinite settings, with the classical and constructive views. Alternate formalisms of nonmonotonic logic, specifically Default Logic and Logic Programming, are discussed in the sixth chapter. We show the equivalence of these formalisms to nonmonotonic rule systems and view some of the results of the previous chapters in terms of these. Lastly, in the seventh chapter we consider possible applications of the results and future directions of the research. CHAPTER 2 THE FINITE CASE In this chapter we consider only those nonmonotonic rule systems which have at least one but only finitely many extensions and/or a finite language. We consider nonmonotonic rule systems in the classical view and also in the constructive view. The underlying logic for a nonmonotonic rule system U =<U,N > can be any form of logic desired. We will often take U to be the set of sentences of some propo- sitional language. The usual monotonic rules of propositional logic are implicitly included in each nonmonotonic rule system unless otherwise stated. We will choose only one representative for each sentence in some systematic way so that there are not infinitely many representations for each sentence in U. For example, -« V ~^b is identified with -i(a A b). 2.1 Finite Classical Nonmonotonic Rule Systems We consider a single nonmonotonic rule system U that has a finite number of extensions and/or a finite language. We intend to explore the following question: If <j) is a formula of the language L, such that <j> 6 S for every extension S of U, then what, if anything, can be said about the theory and/or the formula and its derivation in each extension. We would like to find a single rule that generates in every extension. It would be most useful if the rule could tell us, through premises and restraints, exactly what is required to derive 4> in the system. This rule need not be in the set N of nonmonotonic rules, but it would be desirable to retain the same set of extensions upon adding this rule into N. 18 19 We might first consider the simplest possible form of the common derivation, namely taking <j> as an axiom : /(f). This will certainly generate <j> in every extension, but we may gain new extensions when the rule is added to the set N of rules. Example 2.1.7 Let U =< U,N > be the nonmonotonic rule system where U = {a, b, c} and N = {: {a, c}/b; : {b, c}/a; aVb: {a, b}/c}. This system has two extensions Si = {a}, and S 2 = {b}. The sentence a V b appears in each extension. The axiomatic common derivation for aV b will be : /0V6. Adding this rule to the set N of rules will produce a third extension S 3 = {a V b, c}. This formulation does not accomplish the purpose of the common derivation in that it tells us nothing about what premises and restraints are involved in deriving <j> in the various extensions of the original system. Thus, we consider other forms. Definition 2.1.11 Let U =< U,N > be a finite nonmonotonic rule system. Then U has finitely many extensions, S\, ..., S m . Suppose that G U appears in every Si. Define the support-based common derivation d^ for (j) in U by ^=:{AA...A/? m |A£S t }/0. Example 2.1.8 Letting U be the nonmonotonic rule system where U — {a,b} and N = {: ^b/b; : &/-*; : /a} we will have two extensions, Si = {a, b} and S 2 = {a, ->&}. The intersection of these is {a} . Thus there are eight sentences not in Si and eight sentences not in S 2 ■ Hence there are 64 sentences of the form fa A fa, where Pi £ Si and (3 2 $ S 2 . Some of 20 these will be trivially false, such as ->b A b. Some others will contain that which is in neither extension such as -ia A ->a which will collapse to just ->a. The rest will be restraints of a"*'. We see how the support-based common derivation becomes very large very quickly. This will be a disadvantage. We nevertheless get the following result: Theorem 2.1.12 Let U =< U,N > be a finite nonmonotonic rule system. ThenU has finitely many extensions. Suppose a sentence 4> £ U appears in every extension of the system. Let d^ be the common derivation of <f> as defined in Definition 2.1.11. Then, d^ applies in every extension of the system U and £(U) = £(<U,Nu{d*} >). Proof: Let U =< U, N > be a nonmonotonic rule system with finitely many extensions Si , ..., S m . Suppose a sentence <f> e U appears in every extension of the system. Let rf* be the common derivation of (j) as defined in Definition 2.1.11. Consider an arbitrary extension Sj oiU. Take any conjunction &A...A/8U such that (3{ $ S t . Then fy <£ Sj so that the conjunction (3 x r\.../\f5 m is not in Sj and thus none of the restraints of d* is in Sj. Thus d? applies in Sj and therefore it applies in every extension of the system U. We now have that £(U)CS{<U,Nu{dfi} >). To show that we retain the same set of extensions, suppose that S is an extension of < U, N U {d*} > that is not an extension of U. Then S is not S t for any i e {l,2,...,m}. Since S is not an extension of U the new rule must apply in S . The set of extensions of U is noninclusive so that there exist ip x , ..., tjj m e S such that tpi £ Si. Since we have implicitly included the rules of propositional logic, we have that xpiA...AijJ m eS . By the definition of d 4 ", this conjunction is a restraint of 21 d?. Thus the rule d? does not apply in So contradicting that So is a new extension. Thus, €{U) = £{<U,NU {&}>). Similarly, we might construct a rule consisting only of premises and a conclu- sion. The advantage of this form of the common derivation is that it reveals, at least in part, what is involved in deriving <fi in the extensions. The disadvantage is that we must first know the extensions of the system before we can construct the rule. Finding this rule takes considerably more time than would a rule which relied only on the system U without having to find the extensions. Also, this rule would not be possible in the infinite case. Thus we seek a form of the common derivation that would be based on the rules of the system itself, not the extensions, and would also be possible in the infinite case. We find the following form. For a sequence of sets A\, . . . , A m of sets of formulas, let f\ t A x denote the set of conjunctions a x A . . . A a m where each a t e A x . Let A{A t denote the usual conjunction where the formulas of Ai are themselves conjuncted to form formulas. The notations \J \ Ai and VjA; are similarly defined. Definition 2.1.13 Letting U be a nonmonotonic rule system with a finite language L, we will have a finite number of extensions. List the extensions as {Si, . . . , S m }. Let pi be the proof scheme deriving (j) in the extension Sj and consider the last rule, fj in each Pi. Define the standard common derivation to be d/ be the nonmonotonic rule i We will henceforth refer to the nonmonotonic rule system, < U, A r U{d (/) 1 } >, asU + . 22 Theorem 2.1.14 Let U =< U,N > be a nonmonotonic rule system with a finite language L. Then, for every sentence <fi S (~)£(U), there exists a standard common derivation d^ x that generates <j) in every extension ofU. Proof: List the extensions of U as {S\, . . . , S m }. Suppose that <fi is a sentence oft/ that appears in every extension of the system. Since <j> appears in every extension of the system, there must be a proof scheme pi for each S{ deriving <f> in that extension. List the proof schemes for 4> as {pi, ..., p m }. Consider the last rule, r { = P(r t ) : fa 1 , ..., /3 tt l /<f) of each proof scheme Pi. Let d^ 1 be the nonmonotonic rule V i P(r t ):/\R(r i )/+. i Let Si be any extension of U. We only have to show that d/ applies in $. Since Si is an extension of U, we have that the last rule r% of the proof scheme Pi applies in St. Thus, P( ri ) 6 St and ft', ..., fa* $ Si. Therefore, P(n) = y l P{r l ) e s t . For any 8 x /\...t\5 m € Ai^(n), <5» = P\ for some t, so S t £ S ( and by the standard propositional logic, d/ applies in Si and concludes c(d/) = <j>. The common derivation of any formula <f> in U may not be found in N as illustrated by the nonmonotonic rule system of Example 1.3.3. Recall that N = {:{a}/b,:{c}/b,:{a}/c,:{c}/a}, and that U has the two extensions S\ = {b, c) and S 2 = {b, a}. Also, as before, GD(N,S 1 ) = {:{a}/b,:{a}/c} and GD(N,S 2 ) = {:{c}/b,:{c}/a}. 23 There is no rule of N that derives b in both extensions. However, we may consider the common derivation of b in U which is d\ =: {(a A c)}/b V 6 =: {(a A c)}/b. Then, rf 1 ^ will generate b in each of these extensions. To see this, note that d x b has no premises, and a A c £ S since in S\ we have that a £ S\ since : {a)/b applies in S\. In St, c £ S 2 since : {a}/b applies. Let U —< U, N > be an nonmonotonic rule system with a sentence 4> occuring in every extension of the system. Let d/ be the common derivation as defined in Definition 2.1.13. We find that the sets of extensions of the original system U and the set of extensions of the new system U+ will, under sufficient conditions, be the same. However, U + may have an extra extension, while still having as extensions all the extensions of U. Theorem 2.1.15 Let U =< U,N > be a nonmonotonic rule system with a finite language L such that a sentence <j) e U appears in every extension of the system. Let d^ be the common derivation of (j) as in Definition 2.1.13. Then, E{U) C £{U + ). Proof: Let U =< U, N > be a nonmonotonic rule system with a finite lan- guage L and suppose that a sentence <j> € U appears in every extension of the system. Let dj, be the standard common derivation of (j) as in Definition 2.1.13. Let S be any extension of U. Then, to show that S is an extension of U + , we need to show that for any u G U, u G S if and only if there is a proof scheme p for u in the new system such that all premises in p are in S and all restraints in p are outside of S. Suppose first that u e S. Since 5 is an extension of the system U, there is a proof scheme p for u such that all premises in p are in S and all restraints in p are outside of 5. 24 It is clear that p is still a proof scheme for u in the new system U + . Next suppose that p is an 5-applicable proof scheme in U + . It suffices to consider the last rule r of the proof scheme p where the premises of r are in S, the restraints of r are not in S, and the conclusion of r is u. If r is the common derivation then u = <f> so the <fi e S by the hypothesis. Thus, S is an extension of U + . Hence, £(U)C£(<U,NU{d^ 1 } >). We can generalize this result in the following way. Theorem 2.1.16 Let U =< U,N > be a nonmonotonic rule system with a finite language L such that a sentence 4> G U appears in every extension of the system. Let r^ be any nonmonotonic rule concluding <f> such that r^ applies in every extension of U. Then, £(U)C£{<U,Nu{ r<j> }>). Proof: The proof of this theorem mimics that of the previous theorem. The key part of the proof showing that an extension S of U is closed under the expanded system U + follows as above since the conclusion 4> of the new rule r^ is assumed to be in every extension of U. We see that the sets of extensions may or may not be equal in that the new system U + may or may not have one or more extra extensions. Recall Example 1.3.3. Consider the nonmonotonic rule system U where U = {a,b, c}, N = {: a/b, : c/b, : a/c, : c/a}, and U has the two extensions S\ = {b, c} and 52 = {b, a}, and the common derivation of b in U is d x h =:oA c/b. Adding this new rule to N, we see that < U, N U {d l b } > has the same extensions 5 X and 5 2 , since applying d x b does 25 not prevent the application of any rule in N or allow the application of any rules in the system that were not previously applied. To be precise, suppose there was a new extension S different from S\ and 52- Then, the new rule d 1 ^ must be generating for S. This implies that b € S and (a Ac) £ S. It follows that either a £ S or c <£ S. Thus, one of the original rules, either : {a}/b or : {c}/b, will generate for S and either : {a}/c or : {c}/a will also generate for 5. Then, either c e S or a e S, but this means that either Si C S or S 2 C S. By the noninclusive property, either S = Si or S = S 2 . Example 2.1.9 Now consider the nonmonotonic rule system U where U = {Pi,P2,Ci,c 2 ,a} and N = {pi\ /ci;p2 : /w- a,pi/p2',: a,p2/pi;: pufr/pi Vp 2 ;ci V c 2 : c u c 2 /a}. This theory has two extensions, Si = {P2,C 2 }, and S 2 = {pi,ci}. The formula c\ V c 2 is in each extension and we find that r\=Pi'. /c 2 , and so that r 2 =Pi- /ci, ^civcz =Pi Vp 2 : /ci Vc 2 . 26 Then, S x and S 2 are both extensions of < U, NU {d} ClVC2 } >, but this new nonmono- tonic rule system will have a third extension S = (pj Vp 2 ,ciVc 2l o}, which is not an extension of the original system U. In the previous example, 5 3 is the only new extension obtained by adding the common derivation to the set of rules. To see this, let S be any new extension. The common derivation must generate for S, else S is an extension of the original system. Thus, we have that p x Vp 2 E S so that the conclusion c x \Zc 2 is in 5 as well. If p Y e S, then c x E S by the rule p x : fc\ so that S\ C S, a contradiction to the noninclusive property of extensions, since S is not an extension of the original system. Similarly, if p 2 E S, then c 2 E S so that S 2 C S, a contradiction. Thus, neither of p x or p 2 is in S. Also, if a is not in S, then the rule : {a,p 2 }/p x applies to conclude p x in S. Thus, a E S. From this we now have that 5 3 C S so that 5 3 = S since extensions are noninclusive. Thus, there is only the one new extension. Since the standard common derivation is based on the rules in the proof scheme of (j) instead of the extensions of the system, it might be possible in an infinite system. The good news is that the set of extensions of the new system contains the set of extensions of the original system. The bad news is that these sets of extensions may not be equal. We would prefer that they be equal. We see that this form of the common derivation does not reach the goals that we were after, although interesting. We strive further towards the goal of equal sets of extensions in the next chapter. If we have a formula appearing in some but not all the extensions of U, we may in the same fashion as Definition 2.1.13 create a common derivation for that generates <j> in each extension of U in which it appears. However, we find that in this case Theorem 2.1.15 becomes false, as the next example illustrates. 27 Example 2.1.10 Let U =< U,N > be the nonmonotonic rule system where N = {: {ai,a 2 }/a 3 ,: {a 2 ,a 3 }/a x ,: {a 1 ,a 3 }/a 2 , Pi : { _, ai}/ci,P2 : {^a 2 }/c 2 ,a 3 : jp x Vp 2 ,a x : M,a 2 : /p 2 }. 77iis theory has as three of its extensions, Si = Cn({a 3 ,pi Vp 2 }), 5 2 = Cn({a 2 ,p 2 ,c 2 }), and 5 3 = Cn({a x ,p x ,c x }). We see £/ia£ i/ie formula c x V C2 is in both S 2 and S3, but is not in S\. We find the standard common derivation for c x V c 2 to be d\ x \, C2 =P\ Vp 2 : {-1(01 V a 2 )}/c l V c 2 . Adding this new rule to the set of rules N , we find that both S 2 and S3 are extensions of the new nonmonotonic rule system < U, NU {d} Cl \/ C2 } >. Si, however, is not an extension of < U, N U {d 1 Cl vc 2 } > since it it no longer closed under the set of rules. It is important to note that S\ is a subset of {a 3 ,p x Vp 2 , C\ Vc 2 } which is an extension of<U,NU{d l ClVCi } >. Theorem 2.1.17 Let U =< U,N > be a nonmonotonic rule system with a finite language L such that 4> appears in some but not all of the extensions and each gener- ating rule for each extension S is a generating rule for SL){(f>}. Consider d}^ to be the common derivation of(f> as defined in Definition 2.1.13. Then, for any extension S of U, such that <j> € 5 there is an extension S + ofU + such that S = S + . Furthermore, any extension oflA + which is not an extension ofll must contain <j>. 28 Proof: Suppose that U is a nonmonotonic rule system with a finite language L such that (f> appears in at least one, but not all of the extensions. Consider d 1 ^ to be the standard common derivation of <f> as defined in Theorem 2.1.13. If 4> appears in only one of the extensions of U, then the common derivation d 1 ^ is found in N so that < U,N >= U + , and the theorem is trivially true. Thus, suppose that $ appears in at least two extensions of the nonmonotonic rule system U, but does not appear in every extension. Let $ be an extension of U. If $ is an extension of the new system U + , we are done. Also, if is in $, then $ is clearly an extension of < U, N U {d 1 ^} > as in the proof of Theorem 2.1.15. Hence, consider the case in which S is an extension of the new system U + , but is not an extension of the old system U. If d 1 ^ does not generate for S, then S = GD{N U {d\}, S) = GD(N, S) so that S is an extension of the system U, a contradiction. Thus, d 1 ^ generates for Si so that <P = c(d\) e c(GD(N U {d\}, S)) = S. The added conditions of this theorem that require each generating rule for each extension S to be a generating rule for S U {$} are necessary for the following reason. If we consider the previous example, and add the rule a 3 : /-.(ci V c 2 ) to the set ./V of rules, S\ becomes S\ = {a 3 ,pi Vpa,-i(ei Vc 2 )}. Then, ci V c 2 cannot be added to Si. Now we explore the question of what happens if we take the process further; finding the intersection of the extensions, creating a common derivation, and then adding that rule to the nonmonotonic rule system, over and over. 29 Suppose we let Ii be the intersection of all the extensions of the original nonmonotonic rule system U. Then, in Example 2.1.9 h =Cn({(p 2 Ac 2 )V(p 1 Ac 1 )}). We consider the new rule system U 2 =< U,N 3 >=< U,Nu{d\ x v C2 } > and the set I 2 of all conclusions common to every extension of U 2 . We find that h = Cn({( Pl Vp 2 ) A (c, Vc 2 )}) C h. Moreover, we could choose a conclusion common to all the extensions of U 2 , such as pi Vp 2 . This has the common derivation rf 2 Pl v P2 =: {oVpi,oVp2,o,pi Vp 2 }M Vp 2 - In any new extension S of U3=<U,N 2 U{d 2 PlVp2 } > that was not an extension of the theory U 2 , this common derivation must apply. Sim- ilarly to the previous argument, none of pi,p 2 , ci or c 2 can be in S else we contradict the noninclusive property of extensions. p x V p 2 must be in S since the common derivation applies. Thus, by the common derivation for c x Vc 2 , we conclude c x V c 2 in S and thus a is in S by the appropriate rule from N. This is a contradiction since the common derivation requires that a not be in S. Thus, there are no new extensions, that is, U 2 has the same set of extensions as U3. On a different note, we may force the intersections I x and I 2 to be equal by taking <f>tobef\Ii. This appears in every extension of U. Letting Ni = Nu{d l +}, 30 we find that if S is any new extension, then € S since the common derivation must apply (else S is not new). We then get the following theorem. Theorem 2.1.18 Let <f> be the conjunction of the intersection I x of all extensions of U. Then the intersection I 2 of all extensions ofU + equals Iy. Proof: Clearly we have that I 2 C I x . Now suppose that ip € /j and let S be any extension of U + . If S is an extension of U then tp G S since xjj e I\. Thus, suppose that 5 is an extension of U + that is not an extension of the original system U. This new extension must contain </>. Since <fi is the conjunction of the intersection of extensions I\, we have that <j) — > ip. Thus the extension S must contain i/j. Thus, 1% = h- We may consider any nonmonotonic rule system U, and the set h = f]e{U). For every <fi in this set, we can find a common derivation d x $ which generates in each extension S of U. Consider the nonmonotonic rule system U 2 defined by <U,Nu{d l t\<fieh}>. We may then repeat the procedure to find I 2 = f)£(U 2 ), and if this set is not empty, then we can find common derivations d 2 ^ for any <j> in I 2 such that d 2 ^ generates <j> in every extension S of U 2 . Then, we may consider the nonmonotonic rule system Ui defined by <U,N 2 U{d\\(t>^I 2 }> . We continue this construction by, assuming that U n is defined, let I n = S{U n ). 31 Then, letting d% be the common derivation for <f> £ I n in U n , we define U n+ y to be <^iV n U{(T^ €/„}>. This may be continued until I k is empty for some k and/or N k = Ni for all I > k for some k. This inductive definition begs the following questions. Is there a limit to this process, i.e., is there always some k for which I k is empty and/or JV fc = N t for all / > A;? Does it make a difference if we work in the case where N is finite versus countably or uncountably infinite? These questions should be investigated. Example 2.1.11 Consider the nonmonotonic rule system of Example 1.3.3. Using this nonmonotonic rule system, we would find N 2 to be N U {d\} = {: {a}/b, : {c}/b, : {a}/c, : {c}/a, : {(a A c)}/b). U2 has the same extensions as U so that I 2 = h = {b} and d 2 b = d l b- Then N k = N 2 for all k > 1 . Remark 2.1.19 By Theorem 2.1.15, we have that E(U) C S(U 2 ) C ... C £{U n ) C £(Un+i) C .... For a finite language, or just a finite 7 1; we must eventually have 7 n+1 = /„ for some n. At this point, we find that we will have a common derivation in N n for each <j> G /„, when we consider N n to be defined using all of the common derivations for conclusions in /„_!. U n will be said to HAVE common derivations. Theorem 2.1.20 For any nonmonotonic rule system U with finite I\ or with finite N, there exists an n such that U n has common derivations, and li n is equivalent to the nonmonotonic rule system U n+ k for any k. 32 For an alternate approach, we might consider the nonmonotonic rule system U and the set I\ as before. However, we may choose one element cf> from I x and define < U,N 2 > to be the nonmonotonic rule system U + as seen for Example 6.3.26. We may then consider the set of all formulas which appear in every extension of < U,N 2 >, choose some V among those, and define <U,N 3 > to be <u,N 2 u{d\}> . We may continue in this way with the same result as in Theorem 2.1.20. 2.2 Finite Constructive Nonmonotonic Rule Systems Again, consider a single nonmonotonic rule system U with a finite set of ex- tensions and/or a finite language. In this section, we consider the same question about nonmonotonic rule systems as in the previous section, but use a constructive approach. That is, we consider that pVq is not derived unless one of p or q is derived. Note that we will no longer implicitly assume the propositional axiom pV->p. Had we chosen to keep this axiom, while considering a constructive view, all the extensions of every system would be complete, and consequently uninteresting. We will, however, keep the propositional rules for conjunctions as we did in the classical case. Again, we consider 0, a formula of the language L such that <j> e (~)£{U). Then ^ G 5 for every extension S of U. Since each extension S is of the form c(GD(N, S)), there must be, as before, a proof scheme pi deriving for each extension St. The advantage of the constructive approach is that it allows us to view each set of restraints as a single formula instead of as a set of formulas. Then, instead of asking if each element of the set of restraints is not in a context, we would ask if the restraint itself is not in the context. As it stands, the last rule r t in each proof scheme 33 Pi has as its restraints the set {(3\, ...,#**} for some /?v formulas of the language. We may instead let R(n) = /3\V ... Vf3\. Then flfa) is in the extension S t if and only if |9j e Si for some j, a contradiction since r, generates for Sf. We find that several of the theorems of the last section still hold. Theorem 2.2.21 For any formula <f> of the finite language L such that (j) 6 f\£{U), 4> has a common derivation d 1 ^ which generates (/> in each extension S ofU where U is a constructive nonmonotonic rule system. Proof : Suppose U is a constructive nonmonotonic rule system with a finite language L. Suppose further that <f> is a sentence of U that appears in every extension of the system. List the extensions of U as Si, . . . , S m . Then for each extension 5 8 of U there is a proof scheme p t deriving in S t . Consider the last rule, r t = P(n) : ft*, ..., 0ti % /4 of each proof scheme p { . Let d/ be the nonmonotonic rule ^P^-.^RirJ/cf). i Let Si be any extension of U. We only have left to show that d/ applies in St. Since Si is an extension of U, we have that there is some proof scheme p { that derives in S^ Since this proof scheme derives in $, each rule in the proof scheme applies in S t so that r t applies in Si. Thus, P(r t ) e S z and ft*", ..., ft.' <£ S { . Thus, P(n) = ViP(n) e s t and any ^A...A(5 m 6 A* Rfc) will not be in S t . Thus, d/ applies in 5, and concludes c(d/) = <^>. Thus, for any formula 4> of the language such that G f|£(^), </> has a common derivation d 1 ^ which generates <\> in each extension S of W. Note that d\ may be in TV, but then U + will have the same set of extensions as U. 34 Example 2.2.12 Consider the nonmonotonic rule system of Example 1.3.3. Under the approach of this section, we let N = {: a/b, : c/b, : a/c, : c/a}. Then the nonmonotonic rule system U has the two extensions Sr = {b )C } and S 2 = {b,a}. Also, GD{N,S l ) = {:a/b,:a/c} and GD(N,S 2 ) = {:c/b,:c/a}. Just as before, there is no rule of N that derives b in both extensions. However, we may condsider the common derivation ofbinU by the methods of this section, which is d\ -. (oAc)/6. Then, d l b will generate b in each of these extensions. Compare this version of the common derivation of b in U to that of the previous section where we had d\=:{(aAc)}/b. We see that the two methods produce very similar results, but that the common deriva- tion produced by the methods of this section is computationally simpler. By the same arguement as in Theorem 2.1.15, we still have that S{U)CS{<U,Nu{d\}>) 35 for any e f\S(U). Equivalently, £{U) C £(< U, NU {d^} >), for any € f)£(U). Also as before, the converse of this theorem is false, as illustrated in example 2.1.9. We must then ask if there might be a better formulation of the common derivation that would ensure that same set of extensions when added to the system. There is, but it is not without strings attached. Theorem 2.2.22 For any formula $ of a finite language such that € f)S(U), define the strong common derivation d*^ to be V,P(r<) :|J J2(r«)M i Then, rf% e GD(N U {d* <t> },C]£(U)). Proof : Let be a formula of the language such that e f]£{U). Consider <J% as defined above. Clearly d% £ N U {d*^}. Now, for every extension $ in £{U) we have that some proof scheme p t generates in S t so that P{ri) G S t . Thus, P{d\) = V l P(r l ) e f\£(U). Lastly, we have that /*(<*%) = (J^,-) C f)£(U) if and only if Rfa) C f|£(W) for all ». However, this is if and only if R(n) C 5 2 for some extension $ where Pi generates for 5,-. Then, flfo) 6 5,, a contradiction. So we have that R{d* (j) ) is not a subset off\£(U). Thus d% generates <f> in f|£(W). Note that although this new rule generates for the intersection of all the ex- tensions, it may not generate for each particular extension. Example 2.2.13 Consider the nonmonotonic rule system U where N = {:{a}/b,:{b}/a}. This rule theory has two extensions, Si = {b}, 36 and S 2 = {a}. We have that the formula a V b is in both of the extensions and we find that d* a vb ='■ {a, b}/a V b. By the theorem, d* aVb generates for the intersection of the two extensions. However, it does not generate for either of the extensions Si or S 2 since b € S\ and a e S 2 , respectively. We may again inductively define the nonmonotonic rule system U n as we did in the last section. Investigations into the questions raised by this definition are further warrented in this setting as the common derivations are computationally simpler and the constructive view may make the difference in what the answer to those questions will be. Example 2.2.14 Consider the nonmonotonic rule system of Example 1.3.3. Using this rule system, and the methods of this section, we would find N 2 to be N U {d\} = {: a/b, : c/b, : a/c, : c/a, : (a A c)/b). Again, U 2 has the same extensions as U so that I 2 = h = {b} and d 2 b = d\. Then N k = N 2 for allk > 1. 2.3 Characterizing the Set of Extensions Now, since the intersections of families of extensions are of particular interest, we might ask which families of extensions have intersections which yield a specific theory. Knowing this, given a theory which we desire to see as the intersection of extensions we may create the nonmonotonic rule system whose extensions intersect to yield that theory. Note that we will not implicitly assume any rules of propositional logic for the case of this construction. 37 Theorem 2.3.23 Given any finite family of sets F = {Ti,T 2 , . . .,T n }, in the language L there is a nonmonotonic rule system U whose set of extensions £{U) is exactly F. Proof: Let F = {T X ,T 2 , . . . ,T n }, be any finite family of sets. We create the system U in the following way. Let U be the set of atoms of the language L. Let N = {:{A j T j \j^i}/AT i \l<i<n}. Then, U will have F as its set of extensions. For example, for the family {{a, b, c}, {a, c, d}, {a, b, d}} we would choose the nonmonotonic rule system < U, N > where N = {: {aAbAc,aAc/\d}/aAbAd;: {aAbAc,aAbAd}/aAcAd;: {aAbAd,aAcAd}/aAbAc. This system will have exactly the three extensions: {a, b, c}, {a, c, d}, and {a, b, d}. So we see that any given theory may be derived as the intersection of a set of extensions by determining what family of sets intersects to yield the desired theory, and then constructing the appropriate nonmonotonic rule system whose extensions are that family. The constructive case will be different only in that the number of possible extensions that are acceptable is greatly reduced. This is explored in detail in terms of Default Logic in Chapter 6. CHAPTER 3 THE INFINITE CASE In this chapter we consider nonmonotonic rule systems with infinitely many extensions and an infinite language. This necessitates the concept of a locally finite system as seen in the introduction. We first consider nonmonotonic rule systems in the classical view and then in the constructive view. Lastly, we consider the task of characterizing the set of extensions of a locally finite nonmonotonic rule system. 3.1 Locally Finite Classical Nonmonotonic Rule Systems Considering locally finite nonmonotonic rule systems, we can have results for the infinite case similar to those of the finite case. We should note, however, that the support-based common derivation d? as shown in the finite case is no longer possible in the infinite case since it would result in an infinite conjunction in the restraints of the rule. Still applicable, however, is the standard common derivation d 1 ^. Theorem 3.1.24 Let U =< U,N > be a locally finite nonmonotonic rule system. Then, for every sentence <j> € f\€(U), there exists a standard common derivation d/ that generates 4> in every extension ofU. Proof: Suppose U is a locally finite nonmonotonic rule system. Suppose further that $ is a sentence of U that appears in every extension of the system. Since the system is locally finite, we have that there are only finitely many minimal proof schemes for <f>. List the proof schemes for (j) as Dr+ = {p u ..., p m }. Consider the last rule, r { = P(n) : fa 1 , ..., fa*l<$> of each proof scheme ft. Now, since <j) appears in every extension of the system, we have that for each extension S, there is a proof 38 39 scheme that derives 4> in S, call it ps. Since each rule of the proof scheme applies in S, we know that there must be a minimal proof scheme p i: for some i 6 {1, ..., m}, contained in p s that derives <j> in S. Let d/ be the nonmonotonic rule i Let S be any extension of U. We only have left to show that d^ 1 applies in 5. Since S is an extension of U, we have that there is some minimal proof scheme p l e Dr^ that derives (j> in S. Since this proof scheme derives </> in S, each rule in the proof scheme applies in S so that r { applies in S. Thus, -P(rj) € 5 and /V, ■••, /V ^ 5. Thus, P(r>) = s/iPin) e s and any 5iA...A5 m € Ai R( r i) w ^ not De in S. Thus, d$ applies in S and concludes cid^) = $. We must ask several questions concerning how this new rule effects the system U. First, if the system U is locally finite, then what happens when we add in the new rule to consider the system U + . Is it still locally finite? In terms of the sets of extensions, will we find that £{U) = E{U + )1 We find that the expanded system may no longer be locally finite, as seen in the following example. Example 3.1.15 Let U —< U,N > be the nonmonotonic rule system where U = {ai, a 2 , b, d, e] U {ci\i € lj} and N = {ai : /b;a 2 : /&; : a u d/a 2 ;: a 2 ,d/ai;: ai,a 2 /ai Vo 2 ;ai V a 2 ,b: ai,a 2 /d} 40 U{ai V a 2 , b : Oi, a 2 /cj|i G a;} U{cj : Oi,a 2 /e|2 G a;}. This system has two extensions, Si = {ai,b}, and S 2 = {a 2 ,6}. The atom b appears in each and has the standard common derivation d 1 ^ = a\ V a 2 : jb. Upon adding this rule to the set N, we find that the new system provides an infinite number of minimal proof schemes for e. Thus the new system is not locally finite. The problem arises that there may be infinitely many distinct rules concluding a sentence ip G U that are not applied in any extensions and therefore do not enter into the set of minimal proof schemes for tp. However, the addition of the common derivation to the set of nonmonotonic rules may allow these rules to be applicable and thereby the set of minimal proof schemes to be infinite. Then the new system is not locally finite. To mend this problem, we must rid the system of rules that are not applied in any extension prior to the addition of the common derivation. Definition 3.1.25 Call a nonmnotonic rule r G N ACTIVE if it applies in some extension of the rule system U; call the rule DORMANT, if it does not apply in any extension of the system. Call a nonmonotonic rule system U DORMANT if every rule in N is dormant. Call the system PARTIALLY DORMANT if N has at least one dormant rule and at least one active rule. Finally, call the system ACTIVE if every rule in N is active. [Note that if a system is dormant, then it has no extensions.] Theorem 3.1.26 Let U =< U,N > be a locally finite active nonomonotonic rule system such that </> appears in every extension of the system. If d/ is the standard common derivation for <f> in U, then U + is locally finite and active. Proof: Suppose U is a locally finite active nonomonotonic rule system such that <f> appears in every extension of the system. Let d/ be the standard common 41 derivation for </> in U. Consider the nonmonotonic rule system, U + created by adding the common derivation to the set of nonmonotonic rules: Given that the original system is active, we have that every rule in N applies in some extension of U. Since the system < U, N U {d/} > will have the same extensions as the original system, and any extra extensions obtained are such that the common derivation applies, we have that the new system is active. Further, U is locally finite so that the set of minimal proof schemes for any sentence ip 6 U is finite. These sets of minimal proof schemes will remain finite unless applying the common derivation allows the application of an infinite list of rules that conclude some ip 6 U. Suppose this is true. This infinite list of rules must be from N, as the common derivation is the only rule added to obtain the new system. Thus, these rules are active so that each rule is applied in some extension of U. Thus, each rule provides a proof scheme for if) in U. Since each rule is distinct and concludes ip, we have that none of these proof schemes is contained in any other so that there are infinitely many minimal proof schemes for ijj and U is not locally finite, a contradiction. Thus, the new system, U + is locally finite. Let U =< U, N > be a nonmonotonic rule system with a sentence 4> occuring in every extension of the system. Let d/ be the standard common derivation as defined in Theorem 3.1.24. We find that the sets of extensions of the original system U and the set of extensions of the new system U + will, under sufficient conditions, be the same. However, U + may have an extra extension, while still retaining all the extensions of U. Theorem 3.1.27 Let U =< U,N > be a locally finite nonmonotonic rule system such that a sentence (j) e U appears in every extension of the system. Let d 1 be the 42 standard common derivation of (j) as defined in Theorem 3.1.24. Then, £{U) C E{U + ). Proof: The proof for this theorem is similar to that of Theorem 2.1.15. We can generalize this result in the following way, as in the finite chapter: Theorem 3.1.28 Let U =< U,N > be a locally finite nonmonotonic rule system such that a sentence (j) G U appears in every extension of the system. Let r^ be any nonmonotonic rule concluding <j> such that r^ applies in every extension ofU. Then, £(U)C£(<U,Nu{r+}>). Proof: The proof of this theorem mimics that of the previous theorem. We see that the sets of extensions may or may not be equal in that the new system U + may have one or more extra extensions. Consider the following example: Example 3.1.16 Consider the nonmonotonic rule system U from Example 3.1.15. This system has the two extensions S\ = {ai,b}, and S 2 = {a 2 ,b}. The atom b appears in each and has terminal rules r x = a\ : /b, and r 2 = a 2 : /b, so that the standard common derivation is d 1 t = Oi V a 2 : /b. 43 Upon adding this rule to the set N, we find that the new system aquires and extra extension. S\ and S 2 are both extensions of < U, N U {d l b} >, but we will have a third extension S 3 = {ai V a 2 , b, d, e) U {q,\i E u}, which is not an extension of the original system U. In the previous example, S3 is the only new extension obtained by adding the common derivation to the set of rules. To see this, let 5 be any new extension. The common derivation must generate for S, else S is an extension of the original system. Thus, we have that a\ V a 2 € S so that the conclusion b is in S as well. If ai € S, then b £ S by the rule ai : /b so that Si C 5, a contradiction to the noninclusive property of extensions, since S is not an extension of the original system. Similarly, if 02 G 5, then b € S so that 5 2 ^ S, a contradiction. Thus, neither of a^ or a 2 is in S. Then the rules : ai,a 2 /a\ Va 2 and a^V a 2 : Oi, a 2 /cj for each t apply so that Cj 6 S for each ». From this we now have that 53 C 5 so that S3 = S since extensions are noninclusive. Thus, there is only the one new extension. Further, we might try considering active nonmonotonic rule systems, in hopes that this would cure the new system of its extra extensions. This does not help, as seen in the next example. Example 3.1.17 Consider the nonmonotonic rule system U where U~ {PI,P2,JUJ2,C} and N = {pi : ^'i/c;p 2 : ^j 2 /c; : pi/p 2 ; : p 2 /p\\c : ^ji/^j 2 ; c : ->j 2 /^ii}- This system can be taken to be active and has two extensions, Si = {Pi,c,^ 2 }, 44 and S2 = {P2,C,^ji}. c appears in both extensions and we see that d X e = Pi V p 2 : -iji A -»J2/c. Adding this rule to the set N, we find that the new system, < U, N U {d x c } >, has both S\ and S 2 as extensions but also has two other extensions, S3 and S4 where 53 = {Pi,->ji,c}, and 54 = {p 2 ,-\?2,c}. At this point, all possible versions of the common derivation that carry over from the finite classical case have been exhausted. Yet we crave a form of the common derivation that may have better luck retaining the same set of extensions when added to the original set N of rules. We turn then to the following more complex rules. These are constructed with more intricate restraints that are meant to rule out the causes of extra extensions in U + . Definition 3.1.29 We define two new versions of the common derivation, d]((p) and d 2 ((j)) similarly to the definition of d/ in that we consider the last rule in each of the minimal proof schemes of : Suppose U is a locally finite nonmonotonic rule system. Suppose further that is a sentence of U that appears in every extension of the system. Since the system is locally finite, we have that there are only finitely many minimal proof schemes for (j). List the proof schemes for <j> as Dr^ = {p u ..., p m }. Consider the last rule, 45 U = P{fi) : /?i\ ..., Pu/<l> of each proof scheme p { . Now, since (f> appears in every extension of the system, we have that for each extension S, there is a proof scheme that derives <j> in S, call it p s . Since each rule of the proof scheme applies in S\ we know that there must be a minimal proof scheme p t , for some I G {1, ..., m}, contained in p s , i.e. p { ■< p s , that derives 4> in S. Define the refined common derivation di(4>) to be the nonmonotonic rule V^) : /\ R(r t ) U \/(P(rO A [\/ flfc)])/*. i i Further, define the strong refined common derivation d 2 (<t>) to be the nonmonotonic rule ^P(n) : /\ R(n) u /\(P( r< ) a [\/ R(n)])/4>. Taking each rule in its turn, we find different properties. Since (j) belongs to each extension of the system, it follows as usual that < U,N U {di ((f))} > and < U, N U {d 2 {(f))} > each retain the extensions of < U, N >. Considering the rule d\(4>) we obtain the following results: Theorem 3.1.30 Let U =< U,N > be a locally finite active nonomonotonic rule system such that (p appears in every extension of the system. If di((f)) is the refined common derivation for in U, then < U, N U {d\((j))} > is locally finite and active. Proof: Suppose U is a locally finite active nonomonotonic rule system such that (j> appears in every extension of the system. Let d\{4>) be the refined common derivation for <j> in U. Consider the nonmonotonic rule system created by adding the refined common derivation to the set of nonmonotonic rules: <U,Nu{d l {(t>)}> . 46 Given that the original system is active, we have that every rule in N applies in some extension of U. Since the system < U, N U {di((f))} > will retain the extensions of the original system, and any extra extensions obtained are such that the common derivation applies, we have that the new system is active. Further, the system U is locally finite so that the set of minimal proof schemes for any sentence ip G U is finite. These sets of minimal proof schemes will remain finite unless applying the common derivation allows the application of an infinite list of rules that conclude some ip G U. Suppose this is true. This infinite list of rules must be from N, as the common derivation is the only rule added to obtain the new system. Thus, these rules are active so that each rule is applied in some extension of U. Thus, each rule provides a proof scheme for tp in U. Since each rule is distinct and concludes ip, we have that none of these proof schemes is contained in any other so that there are infinitely many minimal proof schemes for ip and li is not locally finite, a contradiction. Thus, the new system, <U,Nl) {di(4>)} > is locally finite. However, using this version of the common derivation, we may not have that di(4>) applies in every extension of the system. The reason for this is that the dis- junction in the restraints, Y^fojAlVflfo)]), cannot be found in any extension of the system. For this to be true, none of the (P(r<) A (V *(*)]) may appear in any extension of the system. This is too much to ask, as we can only be certain that for each extension there is at least one rule r* that applies. There may be one or more rules that do not apply; i.e. there may be a rule r, that does not apply such that P(tj) is in the extension, but some restraint of r, is also in the extension. In that case, P(rj) A [V R(ri)]) is in the extension so that the disjunction V(^)A[\/«(n)]) 47 is in the exension and the common derivation d\ (<j>) does not apply. Considering the strong refined common derivation, d 2 (<f>), we get just the opposite problem. We find that this version of the common derivation applies in every extension of the system, but may create new extensions when added to the set of nonmonotonic rules. Theorem 3.1.31 Let U =< U,N > be a locally finite nonmonotonic rule system such that a sentence $EU appears in every extension of the system. Let d 2 (<f>) be the strong refined common derivation of <j> as defined in Definition 3.1.29. Then, d 2 (</>) applies in every extension of the system U and e(U)C£{<U,Nu{d 2 (<t>)}>). Proof: Let U =< U, N > be a locally finite nonmonotonic rule system such that a sentence e U appears in every extension of the system. Let d 2 (<j>) be the strong refined common derivation of (j) as defined in Definition 3.1.29. Recall that d 2 (<f>) = VtPin) : /\ R{r % ) U /\(P(r z ) A [\/ R{r t )])/ct>. i i We need to show that the premise of the rule is in every extension of the system U and that no restraint is in any extension of the system. Let S be any extension of U. First, consider the premise, VjPfa). Since S is an extension and thus <j> is in 5, we have that there is a minimal proof scheme, p { € Dr^ that applies in S and concludes (f). r t is the last rule of this proof scheme and thus it must apply in S so that its premise, P(n) is in 5. Thus, \/ l P(r i ) is in S. Now we consider the set of restraints, A^)uA(^)A{V^(n)D- Since r { applies in S we have that no restraint in the set R(ri) is in S. Any a e A, Rfc) has the form (5 X n A ... A (3 m jm where ^ g R{ ri ) for each i. Since ^. £ 5, it 48 follows that a £ S. Thus, no restraint in the set f\ t R(ri) is in S and P{r t ) A [V R{r l )} is not in S. Thus, Ai(^( r i) A [V R{n)}) is not in 5 so that no restraints of d 2 {(f>) are in 5. Thus, d%(4>) applies in every extension of the system U and therefore e(u)cs(<u,Nu{d 2 {(j>)}>) by Theorem 3.1.28. Due to some of the same problems as before, we may still gain extra extensions when the common derivation is added to the set N of rules. We now must ask if it is possible to make sure that the sets of extensions will be the same, and if so, what restrictions will be needed. We find that we can ensure that the sets will be equal, and there are several options to do so. Theorem 3.1.32 Let U —< U,N > be a locally finite premise-free nonmonotonic rule system such that a sentence <j> G U appears in every extension of the system. Let d 2 {<t>) be the strong refined common derivation of <f> as defined in Definition 3.1.29. Then, £{U)=S(<U,Nu{d 2 (d>)}>). Proof: Suppose that U be a locally finite premise-free nonmonotonic rule system and let 4> e U be a sentence that appears in every extension of the sys- tem. Let d 2 (<f>) be the strong refined common derivation of as defined in Theorem 3.1.31. Then d 2 (0) =: A<(V^( r *))M B Y Theorem 3.1.31 we know that the common derivation applies in every extension of U. Hence, by Theorem 3.1.31, we have that £(W)C £(<[/, JVu{d 2 (0)}>). We have only to show the reverse inclusion. For any consequence ip in some extension S in the new system, there must be an S-applicable proof scheme for ip. If the last rule in the proof scheme is anything other than d 2 (</>), then it is a rule of the original 49 system and therefore the proof scheme is valid in the original system. Otherwise, d 2 ((f)) is the terminal rule of the proof scheme for ip and hence ip — 4> and this rule applies in S so that Ai(V^( r i)) * s not m &• That is, for some *, (V R{ri)) is not in S so that the premise-free rule r; applies in S. Hence, the proof scheme pi applies in S. In either case, we see that any proof scheme in the new system is a proof scheme in the original system. Therefore S is an extension of U, and £{U) = £(<U,Nu{d 2 (<j ) )}>). Note that in a premise-free system, all minimal proof schemes have just one line. However, the requirements on the rule system need not be this strong, to ensure that the sets of extensions will be the same. There are other options. We then gain the following less restrictive results: Theorem 3.1.33 Let U =< U,N > be a locally finite nonmonotonic rule system such that any sentence in the intersection of all the extensions of the system is premise-free. Suppose that a sentence (/> € U appears in every extension of the system. Let dip be the standard common derivation of <j) as defined in Theorem 3.1.24- Then, S(U)=£(U + ). Proof: Let U =< U, N > be a locally finite nonmonotonic rule system such that any sentence in the intersection of all the extensions of the system is premise- free. Suppose that a sentence <j> E U appears in every extension of the system. Let d^ be the standard common derivation of <j) as defined in Theorem 3.1.24. Then, since the last rule in each proof scheme for <j> are the only rules considered in the construction of the common derivation, we may follow the proof of the case of the system U itself being locally finite and premise-free. 50 We may instead place the requirements on the sentence in question, i.e. on the sentence which appears in every extension of the system. Theorem 3.1.34 Let U =< U,N > be a locally finite nonmonotonic rule system such that a sentence (j> 6 U appears in every extension of the system and is premise- free. Let d/ be the standard common derivation of <j) as defined in Theorem 3.1.24. Then, d^ 1 is premise-free and £{U)=£{U + ). Proof: Suppose that U =< U, N > is a locally finite nonmonotonic rule system such that a sentence 4> € U appears in every extension of the system and is premise-free. Let d/ be the standard common derivation of <j> as defined in Theorem 3.1.24. For any element a of the restraints of d/, a has the form l n A ... A /? m - where p i ji E R(n) for each i, and no 1 h A ... A p m Jm is in S, for any extension S in which the rule applies. We claim that for some i, none of the f3 l H is in S so that the rule n applies. Supposing not, we may choose for each I some 5 t = f3 l in 5. However, we then have that delta x A ... A 8 k e 5, a contradiction. Thus, any proof scheme in the new system may be replaced with a proof scheme in the original system and hence £{U) = 8{U + ). Next, we consider iterating the common derivation as in Chapter 2. Considering the language to be infinite, and taking the common derivation to be either the standard, refined or strong refined common derivation, we still have that L x D l 2 D I 3 D.... We may define I* to be the intersection of all the J n , define iV* to be the union of all the N n , and define £* to be the union of all the sets of extensions of the rule systems <U,N n >. We then find the following: 51 Theorem 3.1.35 /• =()€* Proof: Suppose that <f> e /*. Then, <j> € /„ for all n so that <j>ef)£(<U,N n >) for all n. Letting S be any extension in £* we have that 5 is an extension of <U,N n > for some n so that (j) e S and thus € f]€*. For the reverse containment, suppose that we have <j)Ef)£*. Then, <j> € S for any extension 5 g £* so that e S for any extension S of any <U,N n >. Hence, </><=/„ for any n so that <f>ef)I n = I*. Thus the equality holds. Theorem 3.1.36 £* C 5(< £/, JV* >). Proof: Let S € £* so that 5 is an extension of some < U,N n > and an extension of any <U,N m > for m > n. We want to show that S is an extension of < U, N* >. To do this, suppose that a rule r e N* generates for S. r e N m for some m, and hence for some m > n. Since 5 is an extension of < U, N m > we have that the consequence of r is in S so that S is an extension of < U,N* >. One might ask at this point if we can show that iV* has common derivations or if it does not. This is a point to be investigated. 3J2 Locally Finite Constructive Nonmonotonic Rule Systems In this section, we consider the same question about nonmonotonic rule sys- tems as in the previous section, but use a constructive approach. That is, we consider that p Vq is not derived unless one of p or q is derived, and extensions are not closed under the propositional rule p V ->p, as in the finite constructive case. Say that an extension S is constructive if p V q e S implies that p e S or q 6 S. Note that if a set S conatins p V -»p and is constructive, then S is complete. 52 Again, consider 0, a formula of the language L such that 4> £ f\S(U). Then € 5 for every extension S of U. As before, there is a finite list of minimal proof schemes Dr^ = {px, . . . ,p m } that derive <j> in the extensions of U. For each t let r x be the last (a.k.a. terminal) rule in p { . The advantage of the constructive approach is the same as in the finite constructive case. It allows us to view each set of restraints as a single formula instead of as a set of formulas. Then, instead of asking if each element of the set of restraints is not in a context, we would ask if the restraint itself is not in the context. As it stands, each rule r { has as its restraints the set {(3\, ...,/?* t .} for some /^ sentences of the language. We may instead let R(r t ) = f3\V ... V(3\.. Then R(ri) is in an extension S if and only if /^ 6 S for some j. We find that several of the theorems of the last section still hold. Theorem 3.2.37 For any formula (j) of the language L such that <p e f]£(U), has a common derivation d 1 ^ which generates (j) in each extension S of U where U is a locally finite constructive nonmonotonic rule system. Proof : Suppose U is a locally finite constructive nonmonotonic rule system. Suppose further that is a sentence of U that appears in every extension of the system. Since the system is locally finite, we have that there are only finitely many minimal proof schemes for cf>. List the proof schemes for <f> as Dr^ = {p u ..., p m }. Consider the last rule, r, = P(r\) : ft*, ..., &//</> of each proof scheme p z . Now, since (f) appears in every extension of the system, we have that for each extension S, there is a proof scheme that derives <f> in S, call it p s . Since each rule of the proof scheme applies in S, we know that there must be a minimal proof scheme p t , for some i € {1, ..., m}, contained in p s that derives (/> in S. Let d$ be the nonmonotonic rule ViP{n) : AiR(n)/<j>. Let S be any extension of U. We only have left to show that d/ applies in S. Since S is an extension of U, we have that there is some minimal proof scheme p { 6 Dr 53 that derives (f> in S. Since this proof scheme derives <j) in 5, each rule in the proof scheme applies in S so that T{ applies in S. Thus, P(ri) G S and /V, ..., fi ti x ^ S. Thus, P{rt) = y l P(r l ) G 5 and any 6iA...AS m G AiRfri) will not be in S. Thus, d/ applies in 5 and concludes c(d+ ) = (j>. Thus, for any formula (j) of the language such that <t> G p|£(^0> has a common derivation d 1 ^ which generates <j> in each extension S oili. Note that rf 1 ^ may be in N, but then U + will have the same set of extensions as U. As in the finite case, the classical and constructive locally finite versions of the standard common derivation d 1 ^ produce very similar rules. The difference is that the constructive version is computationally simpler. We may also simplify the strong common derivation. Theorem 3.2.38 For any formula <fi of the language such that G f)£(U), define d\ to be ViP(r t ) : V i i?(r i )/0. Then, d%€GD(JVu{d%},p|£(W)). Proof : Let (j) be a formula of the language such that <f> G f]£(U). Consider <f as defined above. Clearly d*^ G N U {d%}. Now, for every extension 5 in £{U) we have that some minimal proof scheme Pi generates in 5 so that P(7\) G 5. Thus, P{d* <t> ) = ViP{ri) G C[£{U). Lastly, we have that fl(d%) = \Z t R(ri) G f\£(U) if and only if P(r,) G f|£(^0 f° r a ^ *■ However, this is if and only if R(ri) is in every extension. Now let S Q be an extension where the rule r t generates. Then R(r t ) G S , a contradiction. So we have that R{d*^) is not in f]£(U). Thus d* $ generates <f> in r\£{u). By the same argument as in Theorem 3.1.28, we still have that £{U) C £(U + ) for any cj) G f]£(U). Also as before, we may gain extra extensions, i.e., the contain- ment may be strict. 54 Further, we might try considering active nonmonotonic rule systems, in hopes that this would cure the new system of its extra extensions. This does not help, just at it did not help in the finite case, and for the same reasons. However, all is not lost. The mission to attain equal sets of extensions for U and U + is salvaged by returning to the refined common derivation di (</>). The only required restrictions are that the system be locally finite and constructive. Theorem 3.2.39 Let U —< U,N > be a locally finite constructive nonmonotonic rule system such that a sentence <j> € U appears in every extension of the system. Let di((f>) be the refined common derivation of as defined in Definition 3.1.29. Then, £(U) = £(<U,Nl>{d 1 {<p)} >). Proof: Let U —< U, N > be a locally finite constructive nonmonotonic rule system such that a sentence <f> € U appears in every extension of the system. Let di{4>) be the common derivation of <j> as defined in Definition 3.1.29. that S e £{U). Then S is the set of ^-consequences in U of a subset I of U. To show that S € £(< U,N U {di(<j))} >) we need to show that S is the set of S-consequences in < U, N U {di(4)} > of some subset / of U. We let J = I . This is true as previously since (p is in S and the only new rule concludes (p. Thus, we have only to show the reverse inclusion. For any consequence ip in some extension S in the new system, there must be an 5-applicable proof scheme for ip. If the last rule in the proof scheme is anything other than di(<j>), then it is a rule of the original system and therefore the proof scheme is valid in the original system. Otherwise, di((f>) is the terminal rule of the proof scheme for ip and hence ip = <p and this rule applies in S so that Ai(V- R (n)) is not in S. That is, for some i, (\/ R(n)) is not in S. Thus, no restraint of di(4) is in S. Considering the premise of the rule, y l P(R l ), and knowing that the premise is in S since this rule applies, we have that one of the P(R t ) is in S. This 55 is due to the system being constructive. Thus, the rule T{ applies in S. Hence, the proof scheme pi applies in S. In either case, we see that any proof scheme in the new system is replaceable by a proof scheme in the original system. Therefore S is an extension of U, and £{U)=£(<U,Nu{d 2 (<j>)}>). Now we begin to question the usefulness of the standard common derivation d l <p. This version still has its place. Under appropriate restrictions the less com- plex (as compared to d\ (<j))) standard common derivation will yield the equal set of extensions sought. Theorem 3.2.40 Let U =< U,N > be a locally finite restraint-free constructive nonmonotonic rule system such that a sentence <\> 6 U appears in every extension of the system. Let d^ 1 be the standard common derivation of 4> as defined in Theorem 3.1.24. Then, £(U) = £(U + ). Proof: Suppose that U is a locally finite restraint-free constructive nonmono- tonic rule system such that a sentence <j> e U appears in every extension of the system. Let d+ be the common derivation of <j) as defined in Theorem 3.1.24. In this case, d/ = Vi-Pfa) : I4>- By Theorem 3.1.24 we know that the common derivation applies in every extension of hi. Hence, by Theorem 3.1.28, we have that £{U) C £{U + ). We have only to show the reverse inclusion. For any consequence ip in some extension S in the new system, there must be an 5-applicable proof scheme for tp. If the last rule in the proof scheme is anything other than d/, then it is a rule of the original 56 system and therefore the proof scheme is valid in the original system. Otherwise, d$ is the terminal rule of the proof scheme for tp and hence ip = <f> and this rule applies in S. Considering the premise of the rule, ViP(i?j), and knowing that the premise is in 5 since this rule applies, we have that one of the P{Ri) is in S. This is due to the system being constructive. There are no restraints to worry about. Thus, the rule rj applies in S. Hence, the proof scheme pi applies in S. In either case, we see that any proof scheme in the new system is replaceable by a proof scheme in the original system. Therefore S is an extension of U, and €{U) = S{U + ). It is important to note here that being restraint-free automatically makes the rules monotonic, but that this case is still interesting in the context of what we are trying to accomplish. Theorem 3.2.41 Let U =< U,N > be a locally finite constructive normal non- monotonic rule system such that a sentence (j) 6 U appears in every extension of the system. Let d$ be the standard common derivation of (j) as defined in Theorem 3.1.24. Then, £{U) = £{U + ). Proof: Suppose that U is a locally finite constructive normal nonmonotonic rule system such that the sentence 4> € U appears in every extension of the system. Let dtf, be the common derivation of <j) as defined in Theorem 3.1.24. Then, d^ 1 = VjP(rj) : ^/(j). By Theorem 3.1.24 we know that the common derivation applies in every extension of U. Hence, by Theorem 3.1.28, we have that £{U) C £{U + ). 57 We have only to show the reverse inclusion. For any consequence ip in some extension S in the new system, there must be an S-applicable proof scheme for ip. If the last rule in the proof scheme is anything other than d/, then it is a rule of the original system and therefore the proof scheme is valid in the original system. Otherwise, d/ is the terminal rule of the proof scheme for ip and hence ip = 4> and this rule applies in S so that -i0 is not in 5. Considering the premise of the rule, VjP(i?j), and knowing that the premise is in S since this rule applies, we have that one of the P{Ri) is in S. This is due to the system being constructive. Thus, the rule r, applies in 5. Hence, the proof scheme p^ applies in S. In either case, we see that any proof scheme in the new system is replaceable by a proof scheme in the original system. Therefore S is an extension of U. Thus, €(U) = £(U + ). However, the requirements on the rule system need not be this strong, to ensure that the sets of extensions will be the same. As in the classical case, there are other options. Theorem 3.2.42 Let U =< U, N > be a locally finite constructive nonmonotonic rule system such that the intersection of all the extensions of the system is terminally restraint-free. Suppose that a sentence (ft € U appears in every extension of the system. Let d^ be the standard common derivation of 4> as defined in Theorem 3.1.24. Then, €{U) = S(U + ). Proof: Suppose that U is a locally finite constructive nonmonotonic rule system such that the intersection of all the extensions of the system is terminally restraint-free. Suppose further that a sentence </>£[/ appears in every extension of 58 the system. Let d^ be the common derivation of 4> as defined in Theorem 3.1.24. Then, since the last rule of each proof scheme for (f> are the only rules considered in the construction of the common derivation, we may follow the proof of the case of the system U itself being locally finite, constructive and restraint-free. Theorem 3.2.43 Let U =< U,N > be a locally finite constructive nonmonotonic rule system such that the intersection of all the extensions of the system is terminally normal. Suppose that a sentence (f> € U appears in every extension of the system. Let d^ be the standard common derivation of 4> as defined in Theorem 3.1.24- Then, £{U)=S{U + ). Proof: Let U =< U, N > be a locally finite constructive nonmonotonic rule system such that the intersection of all the extensions of the system is terminally normal. Suppose that a sentence <f> € U appears in every extension of the system. Let dj, be the standard common derivation of <j> as defined in Theorem 3.1.24. Then, since the last rule in each proof scheme for (f> are the only rules considered in the construction of the common derivation, we may follow the proof of the case of the system U itself being locally finite, constructive, and normal. Also as in the classical case, we may instead place the requirements on the sentence in question, i.e., on the sentence (p which appears in every extension of the system. Theorem 3.2.44 Let U =< U,N > be a locally finite constructive nonmonotonic rule system such that a sentence € U appears in every extension of the system and is terminally restraint- free. Let d/ be the standard common derivation of <j) as defined in Theorem 3.1.24. Then, d/ is restraint-free and £{U) = E{U + ). 59 3.3 Characterizing The Set of Extensions In the infinite case, we must again ask if, given a family of sets, we can con- struct a nonmonotonic rule system whose set of extensions is exactly that family. The unfortunate answer to this is no. Although the set of extensions of any nonmonotonic rule system is noninclusive (i.e., forms and antichain), not every noninclusive family of sets is the set of extensions for a nonmonotonic rule system. Consider the following example. Example 3.3.18 Let S = {{u t } : % = 0, 1, . . .}, that is, the family of all singleton sets. This is clearly noninclusive. Now suppose that £ were the set of extensions of some rule system U. For the extension {u }, there must be a proof scheme (j) with finite support S and conclusion u . Now just choose some u k <fc S. Then (j) is also applicable in {u k }, which means that {u k } is not deductively closed and is not an extension. The remedy for this is explored in the next chapter, where we are able to successfully characterize the set of extensions of a locally determined nonmonotonic rule system. CHAPTER 4 LOCALLY DETERMINED NONMONOTONIC RULE SYSTEMS In this chapter we consider a special nonmonotonic subcase of the infinte case. We let U be a locally determined nonmonotonic rule system. This has a large impact on the results. 4.1 Locally Determined Nonmonotonic Rule Systems We may obtain a similar result in the case of U having infinitely many exten- sions, if we make some adjustments. To do this, we will first need some preliminaries. Let U =< U, N > be a countable nonmonotonic rule system. For simplicity, we will assume that U is a subset of the natural numbers u) = {0,1,2,...}. Let U = {u < t*i <... }. The informal notion of a locally determined rule system U is one in which the existence of a proof scheme for a sentence u { (or the lack of existence thereof) can be determined by examining only rules or proof schemes involving some initial segment oft/. Given a proof scheme or a rule p, we write max(p) for the maximum of the set {tjttj occurs in <j>}. We shall write JV n for the set of all rules r e N such that max(r) < n and we shall write U n = {u ,...,u n } and refer to the nonmonotonic rule system made up of these two sets as < U n ,N n >. Definition 4.1.45 Let U =< U,N > be a computable nonmonotonic rule system. Say that n is a LEVEL ofU if for every subset S C {u , ...,«„} and alii < n + 1, if 60 61 there exists a proof scheme p such that the conclusion c(p) = U{, and R(p) 5 = 0, then there exists a proof scheme q such that c(q) = Ui, R(q) C\ S — 0, and max(q) < n+l. Theorem 4.1.46 Suppose that n is a level ofU and suppose that E is an extension ofU. Then, £ n = E D {u ,..., u n } is an extension of < U n , N n >. Proof: Suppose that n is a level of U and suppose that E is an extension of U. Let £ n — EC\{u ,..., u n }. Since E is an extension of U, then for any u, G £ n , there is a proof scheme p such that the conclusion of p is Ui and the support of p has empty intersection with E. Thus, in particular, the support of p has empty intersection with £ n so that since n is a level, there exists a proof scheme p Q such that max(po) < n, Po has conclusion Ui and the support of p has empty intersection with £ n . Thus, p is a proof scheme of < U n ,N n >. In the other direction, if i < n and tt t £ £ n , then there can be no proof scheme p of < U n ,N n > such that p has conclusion u t and the support of p has empty intersection with £ n since this would violate the fact that E is an extension of U. Thus, £ n is an extension of < U n , N n >. Corollary 4.1.47 Suppose that n is a level of U and suppose that S C {u ,...,u n } is not an extension of < U n , N n >. Then, there is no extension of E inU such that ED{u ,...,u n } = S. Further, say that U is LOCALLY DETERMINED or "has levels" if there are infinitely many n such that n is a level of U. For a system U that is locally determined, we let lev(U) be the set of all n such that n is a level of U and we write lev(U) = {l < h <••• }• Suppose that U is a recursive nonmonotonic rule system. Then we say that the system HAS EFFECTIVE LEVELS if there is a recursive function / such that for all i, f(i) > i and f(i) is a level of U. 62 Recall that a nonmonotonic rule system is said to be LOCALLY FINITE if for each (j> e U, there are only finitely many ^-minimal proof schemes with conclusion <f>. Recall also that U is HIGHLY RECURSIVE if U is recursive, locally finite, and there is an effective procedure which, when applied to any (f> € U, produces a canonical index of the set of all codes of -<-minimal proof schemes with conclusion <j>. Now, a nonmonotonic rule system U that is locally determined is not neces- sarily localy finite, but the set of extensions of U will nevertheless correspond to the set of infinite paths through a finitely branching tree and similarly the extensions of a nonmonotonic rule system with effective levels will correspond to the set of infinite paths through a highly recursive tree. Theorem 4.1.48 Let U =< U,N > be a recursive nonmonotonic rule system. 1. If U has levels, then there is a recursive finitely branching tree T and a one-to-one degree preserving correspondence between the set of extensions S(U) ofU and the set [T] of infinite paths through T. Also, 2. If U has effective levels, then there is a highly recursive finitely branching tree T and a one-to-one degree preserving correspondence between the set of extensions £(U) ofU and the set [T] of infinite paths through T. Proof: There is no loss of generality in assuming that U — w so that u Q = 0,«i = 1,« 2 = 2,.... Next, observe that for each n, < U n ,N n > has only finitely many minimal proof schemes so that we can effectively list all of the minimal proof schemes p < p x <..., so that 1. If max(p k ) = i and max(p t ) = j and i < j, then k < I. (This says that if i < j the the proof schemes whose maximum is i come before those proof schemes whose maximum is j.) 63 2. If max(p k ) = max(pi) = i,k < I if and only if code(p k ) < code(pi) where code(p) denotes the index assigned to a proof scheme p under some effective Godel numbering of the proof schemes. We shall encode an extension S of the system U by a path n s — (ftfe, jrj,...) through the complete w-branching tree lu" as follows. first, for all i > 0, n 2 i =s (*)• That is, at the stage 2i we encode the information if i belons to the extension S. Next, if n 2 i = then 7r 2i+ i = 0. But if 7r 2i = 1 that is, if t 6 S, then we put ir 2 i+i equal to that g 5 (z) such that p 9sW is the first minimal proof scheme in our effective list of minimal proof schemes such that the conclusion of p gs (j) is i and the support of p qs (i) has empty intersection with S. Clearly S is turing reducible to ir s . For it is enough to look at the values of its at even places to read off S. Now, given an 5-oracle, it should be clear that for each i e 5, we can use an 5-oracle to find q s (i) effectively. This means that ir s is turing reducible to S. Thus, the correspondence between S and n s is an effective degree-preserving correspondence. It is trivially one-to-one. The construction of a recursive tree T C lu" such that the set [T] of infinite paths through T equals the set {n s \S is an extension of < U, N >} is given in [MNR92b]. The key fact needed to establish the branching properties of the tree T is that for any sequence a G T and any i, either a(2i) = a(2i + 1) = or a(2i) = 1 and a(2i + 1) codes a minimal proof scheme for i. We just note that when a proof scheme p = a(2i + 1) does not correspond to a path tt s , then there will be some k such that a has no extension in T of length k. This will happen once we either find a smaller code for a proof scheme or we find some u > i in the support of the proof scheme p such that all possible extensions r of a have t(2u) = 1. Let L k = max({i\max(pi) < k}). It is easy to see that since the system U is a recursive nonmonotonic rule system, we can effectively calculate L k from k. 64 We claim that the tree T is always finitely branching and that if the system U has effective levels, then the tree T is highly recursive. Clearly the only case of interest is when 2i + 1 < k and a(2i) = 1. In this case we will let a(2i + 1) — c where the conclusion of the proof scheme p c is i and the support of p c has empty intersection with l a and there is no a < c such that the conclusion of the proof scheme p a is i and the support of p a has empty intersection with I a . Now suppose that q is a level and that i < q. Then, by definition, there must be a minimal proof scheme p such that max(p) < q, the conclusion of p is i and the support of p has empty intersection with I a . Thus, p = p t for some I < L q . It follows that c < L q where q is the least level greater than or equal to i. Thus, the tree T is always finitely branching. Now, if the system U has effective levels which is witnessed by the recursive function /, then it will always be the case that c < L f(l} so that the tree T will be highly recursive. Corollary 4.1.49 Suppose that the system U is a nonmonotonic rule system with levels such that there are infinitely many n such that < U n ,N n > has an extension S n . Then U has an extension. Proof: Now consider the tree T constructed for the system U as in Theorem 4.1.48. Here we can again construct our sequence of minimal proof schemes p ,Pi, ... recursive in U just as we did in Theorem 4.1.48. We can only conclude that the tree T is recursive in the system U but in any case, T will be a finitely branching tree. Now fix some level n and consider some m > n such that < U m ,N m > has an extension S m . Then by the exact same arguement as in Theorem 4.1.46, S n = S m n {0,...,n} will be an extension of < U n ,N n >. Now consider the node a = (ct(0),... , a(2n + 1)) such that 1. a{2i) =0iU^S n , 2. a{2i) = 1 ifieS n , 65 3. cr(2z + 1) = if cr(2i) = 0, 4. a(2i + 1) = c where c is the least number such that max(p c ) < n, the conclusion of p c is t and the support of p c has empty intersection with S n . It is easy to see from our constuction of the tree T that a eT. It follows that T is infinite and hence T has infinite path tt by Konig's Lemma. But the proof of Theorem 4.1.48 shows that S^ is an extension of the system U. The next quesion is how to ensure that we can get recursive extensions. In particular, suppose that the set of extensions of U is a decidable n°i class, that is, the set of infinite paths through a computable tree T with no dead ends. Then every node of the tree has an infinite recursive extension. If we only assume that the set of dead ends of T are computble, the any node with an infinite extension has a computable infinite extension. Definition 4.1.50 1. Let U =< U,N > be a nonmnotonic rule system with levels. Suppose that {n\n is a level of < U, N >} = {/ < l x <...}. Then we say that U HAS THE LEVEL EXTENSION PROPERTY if for all k, if S k is an extension °f < Ui k ,N ik >, then there is an extension of S k+ i of < U tk+1 ,N lk+l > such that Sk+i n {u ,...,ui k } = s k . 2. A level n ofU is a STRONG LEVEL ofU if for any level m < n ofU and any extension S m of < U m ,N m >, if there is an extension S n of < U n , N n > with S n ^ {uo,...,u m } = S m , then there is an extensions ofU with SCi {u ,..., u m } = S m . 3. U HAS STRONG LEVELS if there is a computable function f such that, for each i, i < f(i) and f(i) is a strong level. The level extension property provides a way to construct an extension of the system U by extending from level to level. The following result is immediate: 66 Theorem 4.1.51 If E is a decidable U°i class of subsets ofU with levels, then there exists a nonmonotonic rule system U with the level extension property such that E is the set of extensions ofU. Definition 4.1.52 We say that a recursive nonmonotonic rule system U with levels has IMMEDIATE WITNESSES if for any levels m < n ofU, whenever there is a set V C {u ,...,u m } such that there is an extension S ofU with Sn {u ,...,u m } = V but there is no extension S ofU such that S fl {u ,...,u m+l } = V, then either (i) there is a proof scheme p with max(p) < m such that the support of p is a subset of {u ,...,u n } - V and p concludes u n+1 or (ii) there is a proof scheme p with max(p) < n + 1 such that the support of p is a subset of {u Q ,...,u n ,u n+1 } -V and the conclusion of p is in {u ,..., u n , u n+l } - V (note: it is easy to see that it must be the case that u n+ i is in the support of p.) One can extend this concept as follows: We say that a recursive nonmonotonic rule system U HAS WITNESSES OF DELAY k if for all n whenever there is a set V C {«„,...,«„} such that there is an extension S of U with S D {u ,...,u n } = V but there is no extension S of U such that S n {u Q ,..., u n+1 } = V, then either (i) there is a proof scheme p with max(p) < n + 1 such that the support of p is a subset of {tio,..., u n ) - V and p concludes u n+ i or (ii) for all sets T C {u n+2 ,..., u n+k }, there is a proof scheme p T with max{p T ) < n + k such that the support of p T is a subset of {u ,...,u n+k } - (T U V) and the conclusion of p is in {u ,..., u n+k ) - (T U V). Theorem 4.1.53 Suppose thatU is a recursive nonmonotonic rule system which has witnesses of delay k for some k>\ and which has at least one extension. Then the lexicographically least extension of the system is recursive. 67 Proof: We can construct the lexicographically least extension S of the system U by induction as follows. Suppose that for any given n we have constructed S n = SO {u ,..., u n ). Then S n+ \ — S n unless either (i) there is a proof scheme p of level n such that the support of p is a subset of {u ,..., u n } — S n and p concludes u n+ i or (ii) for all sets T C {u n+2 ,...,u n+ k}, there is a proof scheme p T of level n + k such that the support of pr is a subset of {u ,..., u n+k } - (TuS„) and the conclusion of pis in {u ,...,u n+k } - (TuS n ). in which case S n+1 = S n U {u„+i}. Note that since there are only finitely many minimal proof schemes of any given level, we can check conditions (i) and (ii) effectively. Since there is an extension, it is easy to see that our definitions insure that S n is always contained in the lexicographically least extension of the system U. Thus, S = [j n S n is recursive. By putting suitable effective bounds on the effective levels and/or the effective witnesses, one can readily come up with conditions that force U to have exponential time, NP, or P-time extensions. This is a topic of current research. 4.2 Common Derivations in Locally Determined Nonmonotonic Rule Systems Let U =< U,N > be a nonmonotonic rule system with infinitely many ex- tensions that is locally finite, locally noninclusive and locally determined (or "has levels"). Suppose (j> G U appears in every extension of U. Since the system is com- putable, we have that <j) - Uj for some j. Since the system is locally determined, there are infinitely many n such that n is a level of U so that we may choose n{4>) to be the least level of U greater than or equal to j. When we restrict each extension of the system to the set {u Q , ...,u nW } we then have only finitely many extensions, 68 call them Si, ..., S m . Then we may define a common derivation df for in U to be df =: {0 1 A.../\0 m \Vi,0 i € {«o, •• .,««(*)}, A £ £}/0- We then get a result similar to the finite case. Theorem 4.2.54 Let U =< U,N > be a locally finite, active nonmonotonic rule system that is locally noninclusive and locally determined. Suppose a sentence $ € U appears in every extension of the system. Let df be the common derivation of as defined above. Then, df applies in every extension of the system U and £(U)=£(<U,Nu{dt}>). Proof: Let U =< U, N > be an active nonmonotonic rule system with in- finitely many extensions. Suppose a sentence 6 U appears in every extension of the system. Let d* be the common derivation of <f>. Consider an arbitrary restricted extension Sj of U. Take any conjunction &A...AJ0U such that ft g S { . Then $ £ S 3 so that the conjunction $ x N...l\$ m in not in 5,- and thus none of the restraints of d* is in S y Thus df applies in Sj and therefore it applies in every extension of the system U. By Theorem 3.1.28 we now have that £(U)C£(<U,Nu{dt} >). To show that we retain the same set of extensions, we need only to show the reverse inclusion. Suppose that So is a restricted extension of < U, JVU {d?} > that does not extend to an extension of U. Then, since U is locally noninclusive, there exist %p u ..., ^ m € S such that ^ g 5,. Then, ViA...AV> m is a restraint of d* Thus, q^A-A^m is not in 5 since df applies in 5 , a contradiction. Thus, £(U) = S(<U,Nu{dt}>). 69 The other notions of the common derivation, the standard common derivation, the refined common derivation and the strong refined common derivation developed in chapter three still apply in locally determined nonmonotonic rule systems by the same theorems. 4.3 Characterizing the Set of Extensions In this section, we shall provide a characterization of the set of extensions of a recursive locally determined nonmonotonic rule system U = (U,J\f). Let £{U) be the set of all extensions of U. Our first observation is that S(U) is closed in the natural topology on subsets of U. Proposition 4.3.55 IfU is locally determined, then £{U) is a closed set. Proof: Let Ei,E 2 , ... be a sequence of extensions with limit E in the usual product topology on sets. Suppose that Ui G E. Then there must be some K such that Ui G Ek for all k > K. Thus for each k > K, there is proof scheme 6 k such that E k C\supp(9 k ) = 0. Now let / be the least level > i. Then since U is locally determined, it follows that for each k > K, there is a proof <f> k of U\ such that E k n supp(<p k ) = 0. But there are only finitely many possible support sets for such proof schemes in Ui so that infinitely many of the (j) k have the same support S. However since SnE k = for infinitely many k, it must be the case S D E = and hence u r e E. Vice versa, suppose that u, ^ E. Thus there must be some K such that for all k > K, Ui £ E k . Suppose by way of contradiction that there is proof scheme (f> with cln{(j)) — Ui and supp(4>) = S with S n E = 0. Since S is finite, there must be some M such that S n Em = for all m> M. But this would mean that </> would witness that u t G E m for all m> M, contradicting our previous assumption. (This direction applies even if U is not locally determined.) We should note however that, in general, £(U) is not a closed set. 70 Example 4.3.19 Let U = {u , u u . . .} and let N consist of the following set of rules: { 2 u^ '■ Vn, A;}. This means that for any extension E and any k, u k 6 E if and only if at least one of the set {u 2 k {2n+1) : n = 0, 1,. . .} is not in E. It is not hard to see that for any k, there will be an extension E ofU which contains all of {u , u u ...,u k }. Thus if £(U) were closed, then U itself would be an extension, which is clearly false, since none of the rules are U -applicable. Hence £{U) is not a closed set. We say that a family £ of sets is noninclusive if for any two sets A, B £ £ , neither A C B nor B C A. A second key property of the set of extensions of a nonmonotonic rule system is that it must be noninclusive. That is, the following holds. Lemma 4.3.56 For any nonmonotonic rule systemU, the set £(U) is noninclusive. However, not every noninclusive family of sets can be the set of extensions of a nonmonotonic rule system. Recall the example given previously. Example 4.3.20 Let £ = {{ Ui } : i = 0, 1, . . .}, that is, the family of all singleton sets. This is clearly noninclusive. Now suppose that £ were the set of extensions of some rule system U. For the extension {u }, there must be a proof scheme <j> with finite support S and conclusion u . Now just choose some u k <£ S. Then 4> is also applicable in {u k }, which means that {u k } is not deductively closed and is not an extension. Thus £ = {{u t } : i = 0, 1, . . .} cannot be the set of extensions of a nonmonotonic rule system. However, by combining the two ideas of closure and noninclusivity, we can define a condition which guarantees that a family of sets is the set of extensions of a nonmonotonic rule system U = (U, N) with strong levels. Given a family S of subsets of U, let S n = {E n {u , ...,u n }:EeS}. 71 Definition 4.3.57 Let S be a family of subsets ofU. 1. We say that n is a level of S if S n is mutually non-inclusive. 2. We say that S has levels if there are infinitely many n such that n is a level of S. 3. We say that S has effective levels if there is a recursive function f such that, for all i, f(i) > i and f(i) is a level of S. There are many examples of families of set of U = {u , tti, . . .} with effective levels. For example, consider the family S of all sets S such that for all n, \S n {u , . . . , i4 2 "}| = n. It is easy to see that for all n, 2" is a level of S. For a more general example, let U be the set of all finite truth table functions on a countably infinite set {a ,a u ...} of propositional variables. That is, for each sentence ip of propositional calculus, U contains exactly one sentence logically equivalent to %jj. These are listed in order of the maximum variable a k on which the sentence depends. Thus, uq and U\ are the (constant) True and False sentences; u 2 and u 3 are the sentences a Q and -*a , u 4 , . . . ,ui 5 list the sentences depending on a and a l5 and so on. Now let T be any consistent set of sentences and let S(F) be the set of complete consistent extensions of T. The levels of 5 = {UnS : 5 6 S{T)} are just the numbers 2 2 - 1. This is because if two sets in S disagree on the first 2 2k - 1 sentences, then there must be some t with i < k such that they disagree on a t , which means that one of the sets contains a* but not ->ai whereas the other set contains -la, but not a { . Thus the two sets are mutually noninclusive. Theorem 4.3.58 IfS is a closed family of subsets ofU with levels, then there exists a nonmonotonic rule system U with strong levels such that S is the set of extensions ofU. Furthermore, if S is a decidable Yl\ class and has effective levels, then U may be taken to have effectively strong levels. 72 Proof: Given the family S, we shall directly construct a nonmonotonic rule system U = (U, N) such that 8{U) = S. First, if S is empty, we let N consist of the single rule *** It is easy to see in this case that U has no extensions. Thus we assume that S / and hence that each S n is nonempty as well. We then create a set of rules for every level n of S. For each level n, let E?, . . . , ££ be the list of all sets of the form En{u Q , ...,u n } for E £ S. Then for each such E? and each c € £?, iV will contain a rule r t<c = &*£&* w h e re {A, . . . , m } = {u , ...,u n }- Ef. It is then easy to see that each E™ is an extension of U n and that n is a level U n . Moreover it easily follows that the set of extensions of U is exactly S. For the second part of the theorem, we use the same nonmonotonic rule sys- tem. We note that decidable n°-class of sets has the property that there is a highly recursive tree T contained in {0, 1}* such that set of infinite paths through T corre- spond to the characteristic functions of elements of S and T has no dead ends, i.e. every node 77 € T can be extended to an infinite path through T. Thus for any level n of <S, the sets EJ, . . . , E% n described above will just correspond the set of nodes of length n in the tree T. Because each of the nodes of length n can be extended to infinite path through T, it follows that each extension E? of U n can be extended to an extension E of U such that £n{%...,u„} = £f. It then easily follows that n is a strong level of U. Thus U will have effectively strong levels in this case. One problem for nonmonotonic rule systems is to determine which sets of extensions can possibly result from some (recursive) nonmonotonic rule system. It is well known that any set of extensions must be mutually non-inclusive, that is, if S and So are two different extensions of the system U, then we can never have S C Sq or S C S. We will sometimes say that the set of extensions has the noninclusive property. On the other hand, for infinite languages, not every mutually non-inclusive set of extensions can be realized. 73 Nonmonotonic rule systems with levels may be used to produce a large family of possible sets of extensions. Given a family F of subsets of U, let F n = {S n {u ,..,u n }\S G F}. Definition 4.3.59 Let F be a family of subsets ofU. 1. We say that n is a level of F is F n is mutually noninclusive. 2. We say that F has levels is there ar infinitely many n such that n is a level ofF. 3. We say that F has effective levels is there is a recursive function f such that for all i,i < f(i) and f(i) is a level of F. Theorem 4.3.60 1. If F is a closed family of subsets of U with levels, then there exists a nonmonotonic rule system U with levels such that F is the set of extensions ofU. 2. If F is a decidable U°i family of subsets of U with effective levels, then there exists a nonmonotonic rule system U with effective levels such that F is the set of extensions ofU. Proof: Observe that if F is empty, then there is a single rule : {u }/u with no extensions. Thus, we may assume that F is nonempty and thus each F n is nonempty as well. For each level n, we have a set of rules as follows. For each S x , ...,S k list the family of intersections Sn{%... , u n ] for S € F. For each partial extension Si and each c € Si, we will have a rule r i|C with conclusion c and with restraints b for each b <£ S t . We know that the rule r i<c must exist since Sj is not a subset of S z by the noninclusive property. 74 We claim that each level n of the family F is also a level of the proof system U. To see this, let T be a subset of {u ,..., u n }, let j < n and let p be a proof scheme with conclusion Uj = en such that p has empty intersection with T. Since the rules of U have no premises, we may assume that p consists of a single rule r = r^ c . Thus, there exists S € F and a level m of F such that S t = S n {u ,...,u m }. If m < n, then max(p) < m < n as desired, on the other hand, if m > n, then consider the restricted partial extension S k = S D {u ,...,u n } and the corresponding rule r k}C as level n. It is clear that S k C Si and that S k fl {u Q ,..., u n } = 5^0 {u Q ,...u n }. Then the support of the rule r fc)C has empty intersection with 5 since max(rk, c ) < n and the support of r fe)C is equal to {u ,..,u n } - S k = {u ,..,u n } -Si which is a subset of the support of r, )C . We need to show that the set of extensions of U is exaclty F. Let us first show that any element S of F is an extension of the system U. Given c e S, the rule r ic has no premises, has restraints all not in S, and has conclusion c. Thus, c has a one line proof scheme. Next suppose that 5 admits some rule r — r k>d . If k = z, then of course d G S, so that S is closed under r. If k ^ i, then by the noninclusive property, r has a restraint b G Si - S k so that 5 does not admit r. Next we show that U has no other extensions. Let S* be any extension of U and suppose that it differs from each S £ F. Since F is closed, there must be a level n such that S* = S* D {«<>,..., u n } differs from each SC\{u ,..., u n }. Otherwise, there would exist, for each level n, some S n such that S* fl {u ,...,u n } = E n n {u ,...,u n }. But then S* = lim n E n would be in F, since F is assumed to be closed. Now there is at least one S G F n and S* * / S by the choice of n. Furthermore, 5* n {u ,..., u„} is an extension of < U n , N n >, by Theorem 4.1.48, since < U n , N n > has levels. It follows that S* n {u ,...,u n } is not a subset of S, by the noninclusive property, so that 5* n {w ,..., u n ) is nonempty. Thus there is some c GS* fl {u ,..., u n ) 75 and therefore S* * admits some rule r i)C where S{ is an extension of F n . But then it follows that S* n {uo,-..,u n } C Si, again violating the noninclusive property. Suppose now that F is a decidable 11° i class and has effective levels. Then for any n, we can compute the set of intersections S D U n for S G F, which will just be the set of paths of length n in the tree T. Now we can effectively compute an increasing sequence of levels and use the set of intersections S fl U n to compute the rules at level n for the desired rule system. It follows from the proof of Theorem 4.1.46 that if U has effective levels and has the level extension property, then the family of extensions of U may be represented as a decidable n°i class. Thus, we have the following results: Theorem 4.3.61 1. Suppose that U is a recursive nonmonotonic rule system with effective levels and has the level extension property. Then for every level n and extension S n of < U n ,N n >, there is a recursive extension of S of U such that Sn{u ,...,u n } = S n . 2. Suppose that U is a recursive nonmonotonic rule system with strong levels. Then for every level n and extension S n of < U n ,N n >, if there is an extension S of U with S n {uo,...,u n } = S n , then there is a recursive extension of S ofU such that SD{u ,...,u n } = S n . CHAPTER 5 COMPUTABILITY AND COMPLEXITY ISSUES In this chapter we show a few results concerning the computability and com- plexity of the common derivations and their associated nonmonotonic rule systems. 5.1 Finding Extensions with Low Complexity Throughout this section, we shall assume that U = (U, N) is a recursive nonmonotonic rule system such that U = u = {0,1,2,- ■ ■}. Moreover if U is locally determined, we let {/ < h < . . .} denote the set of levels of U and if U has strong levels, then we let {s < 5] < • • •} denote the set of strong levels of U. In this section, we shall show how we can use the notions of levels and strong levels to provide conditions which will ensure that U has an extension which has relatively low complexity even when U is infinite. We shall distinguish two represen- tations of U, namely the tally representation of U, Tal(U), and the binary represen- tation of U, Bin(U). In the tally representation of U, we shall identify each n e U, with its tally representation, tal(n), and in the binary representation of U, we shall identify each natural number n with its binary representation, bin{n). Given a rule r = Ql '-"' Q "^i'-" fl m > we let the tally and binary representations of r be given by tal(r) = 2tal{a l )2---2tal{a n )3tal((3 1 )2---2tal{l3 m )3tal{ip) (5.1) bin{r) = 2bin{a l )2 ■ ■ ■ 2bin(a n )3bin{p l )2 ■ ■ ■ 2bin(/3 m )3bin{tp) . (5.2) We then let Tal{N) = {tal(r) : r e N} and Bin(N) = {bin{r) : r e N}. Similarly given a proof scheme r/> = (0 X , . . . , <f> k ), we let the tally and binary representations of 76 77 ip be given by tal(xp) = 4tal(<j> l )4 ■ ■ ■ 4tal(<f> n )4 (5.3) bin(tp) = 4bin((/)i)4 ■ ■ ■ 4bin((j) n )4 (5.4) Finally given a finite set of proof schemes proof T = {ipi, . . . ,tp s }, we let the tally and binary representations of T be given by tal(T) = 5taZ(V>i)5---5taZ(V>,)5 (5.5) bin(T) — 56m(^i)5- • -56m(^ s )5 (5.6) Definition 5.1.62 We say that the nonmonotonic rule system U is polynomial time locally determined in tally, if the nonmonotonic rule system Tal(U) = (Tal(u)), Tal(N)) has the following properties. 1. There is a polynomial time function g such that for any i, g(tal(i)) = tal(l ki ) where ki is the least number k such that l k > i. 2. There is a polynomial time function h such that for any i, h(tal(i)) = tal(Ti) where Ti is the set of all proof schemes Ui k whose conclusion is i where tal(lk t ) = g(tal(i)) Similarly we say that U is polynomial time locally determined in binary, if definition (5.1.62) holds where we uniformly replace all tally representations by binary repre- sentations. We can also define the notions of U being linear time, exponential time, and polynomial space in tally or binary in a similar manner. This given, we then have the following: Theorem 5.1.63 1. Suppose that U is polynomial time locally determined non- monotonic rule system in tally which has the level extension property. If I is a level of U and Ei is extension of Ui such that there is a unique extension E of U with E {0, ...,/} = Ei, then E e NP. 78 2. Suppose that U is polynomial space locally determined nonmonotonic rule sys- tem in tally which has the level extension property. If I is a level ofU and Ei is extension ofUi such that there is a unique extension E ofll with £Tl{0, ...,/} = Ei, then E £ PS PACE 3. Suppose that U is polynomial time locally determined nonmonotonic rule system in binary which has the level extension property. If I is a level of U and Ei is extension ofUi such that there is a unique extension E ofli with £Tl{0, ...,/} = E u then E <E NEXPTIME. 4- Suppose that U is polynomial space locally determined nonmonotonic rule sys- tem in binary which has the level extension property. If I is a level of U and Ei is extension of Ui such that there is a unique extension E of U with EH {0,. ..,/} = E u then E € \J c > {DSPACE{2 nC ). Proof: For (1), suppose that / = l t where recall that the set of levels oiU is {lo < k < . . ■}■ Then for any i > l u consider the level Ik, where g(tal(i)) = tal(l k J. By the level extension property, it follows that there is an extension of Uu , Ei. , such that Eu n {0, . . . , /} = E t . Moreover, it must be the case that E n {0, . . . , l ki } = E tk since otherwise we could use the level extension property to show that there is a sequence of extensions {E^ : j > k{} such that for each j > hi, Ei is an extension of U tj where E X] n {0, . . . , lj- X } — E Xi _ x . One can then easily prove that E' = Uj> ki E { . is an extension of U such that E' n {0, . . . , /} = E t contradicting our assumption that E is the unique extension of U such that E C\ {0, . . . , 1} = E t . It follows that to decide if i € E, we need only guess Ei k ., verify that it is an extension of Ui k , and check whether i G Ei h . We claim that this is an NP process. That is, we first guess the sequence xe, (0)---X£, (4,) where xe, is the characteristic function of Eu. Note that our conditions ensure that there is some polynomial p such that l kt < p(\tal(i)\). It follows that we can compute l ko = 79 g(tal(0)),l kl = g(tal(l)), . . . ,l kl = g(tal(l ki )) in polynomial time in \tal(i)\. Since for each j, l kj is the least level greater than or equal to j, it follows that l ko < l kj < ■• - hi. = hi- Thus if ki — s, we can find Z < ^1 < • • ■ < Z s is polynomial time |ta/(t)|. Note by assumption, t < s. Now consider E r = Eu n {0, . . . ,Q for r = t,t + 1,. . . ,s. By our definition of levels, it must be the case that each E T is an extension of U lr . That is, if x £ E r , there can be no proof scheme ip oiU lr such that cln(ip) = x and supp(ip) n E T — since otherwise ip would witness that x € E s . Vice versa, if x e E r , then x € E, and hence there is a proof scheme 6 X of U is such that cln(6 x ) = x and supp(6 x ) H E, = 0. But since / r is level, there must be a proof scheme t/>* such that max(tp x ) < l r , cln(ip x ) = x, and supp{ip x )n(E s n{0, . . . , / r }) = 0. Thus ip x is a proof scheme which witnesses that x £ E r . Note that if it is the case that / r _! < x < l r , then ip x in r x . Thus since we can also compute h(tal(0)) = tal{V ),h{tal(l)) a ia/(r x ),..., h{tal(l ki )) = tal(T llH ) in polynomial time in |ta/(i)|, it follows that to check that E ik ^ is an extension, we need only verify that that for each x > U, XE, k (x) = 1 iff there is a proof scheme tp x e T x such that supp(ip x ) n E lk = 0. It is easy to see that for each such x our codings of proof schemes and rules is such that we can decode tal(T x ) and check if there is such a i\) x is polynomial time in l ki . Thus we can verify that E lk , is an extension of W Jfc . in polynomial time in \tal(i)\. Hence it follows that E € NP. The proof of part (2) is similar. However since in this case, the length of the sequence xe,. (0) • • • Xe,. (ki) is bounded p(\tal(i)\) for some polynomial p, we do not have to guess it. That is, in p(i) space, we check all strings of {0, l} /fc > to see if they are the characteristic function of an extension E* of U ik such that E* n {0, ...,/} = E t . Since there is only one such extension with this property, we can search until we find it. Thus our computations will require only polynomial space. The proof of parts (3) and (4) uses the same algorithms as in parts (1) and (2). However in this case the string xe,, (0) • • • xe, (lk { ) may be also long a 2 p d 6in WI> 80 for some polynomial P. Thus the algorithm could take on the order of 2' w " (l) l c steps in case (3) and require 2l 6in W |c space in case (4). We should note that if we replace the hypothesis of polynomial time and polynomial space by linear time and linear space in parts (3) and (4) of Theorem (5.1.63) respectively, then we get the following. Theorem 5.1.64 1. Suppose that U is linear time locally determined nonmono- tonic rule system in binary which has the level extension property. If I is a level ofU and Ei is extension ofUi such that there is a unique extension EofU with En{0,...,l} = E h then E e NEXT. 2. Suppose that hi is linear space locally determined nonmonotonic rule system in binary which has the level extension property. If I is a level of U and Ei is extension oflii such that there is a unique extension E ofU with E'flfO, . . . ,1} = Ei, then E <E EXPSPACE. It is easy to show that we can weaken the hypothesis in Theorems (5.1.63) and (5.1.64) that there is a unique extension E of U extending E t to the assumption that there are only finitely many extensions of U extending E\ and obtain the conclusion that all of the extensions of E t are in the same corresponding complexity classes. However if we do not make any assumption about the number of extension of U which extend Ei, then the only thing we can do is try to construct the lexicographically least extension of E t . One can see that in cases (2) and (4) there would be no change in the conclusion. However in case (1), the computations could take 2" c steps and in case (3), the computations could require 2 2 " steps. Finally we note that similar results can be proven using strong levels instead of the level extension property. We state the appropriate definitions and results without proof. Recall that if U has strong levels, then we let {s Q < s x < . . .} denote the set of all strong levels of U. 81 Definition 5.1.65 We say that the nonmonotonic rule system U has polynomial time strong levels in tally, if the nonmonotonic rule system Tal(U) = (Tal(uj),Tal(N)) has strong levels and the following properties. 1. There is a polynomial time function g such that for any i, g(tal(i)) = tal(sk { ) where ki is the least number k such that s k > i. 2. There is a polynomial time function h such that for any i, h(tal(i)) = tal(Ti) where I\ is the set of all proof schemes U Sk whose conclusion is i andtal{l k% ) = g{tal(i)) This given, we then have the following. Theorem 5.1.66 1. Suppose that U is a nonmonotonic rule system which has polynomial time strong levels in tally. If I is a level ofU and Ei is extension of Ui such that there is a unique extension EofU with E D {0, ...,/} = E t , then E e NP. 2. Suppose that U is nonmonotonic rule system which has polynomial space strong levels in tally. If I is a level ofU and E\ is extension ofUi such that there is a unique extension EofU with E n {0, ...,/} = E h then E G P SPACE 3. Suppose that U is nonmonotonic rule system which has polynomial time strong levels in binary. If I is a level ofU and Ei is extension ofUi such that there is a unique extension E ofU with EC) {0, . . . ,1} = Ei, then E e NEXPTIME. 4- Suppose that U is a nonmonotonic rule system which has polynomial space strong levels in binary. If I is a level of U and Ei is extension of Ui such that there is a unique extension E of U with E n {0, . . . , /} = E t , then E 6 U C > (£>SP^C£(2" C )). 82 5.2 Computability and Complexity of Common Derivations Corollary 5.2.67 Let < U, N > be a highly computable nonmonotonic rule system. Then, for every sentence G f]E < u,N>, there exists a computable standard common derivation d^ x that generates (f> in every extension of < U, N >. Proof: Using the standard common derivation defined as in Theorem 3.1.24, the definition of the rule yields an algorithm for constructing it. Since the system < £/, N > is computable we have that each of U and N is computable so that the set of minimal proof schemes, Dr^ for any sentence tp £ U is computable. Hence the common derivation is computable. Theorem 5.2.68 Let < U, N > be a highly exponential time (polynomial time, etc.) nonmonotonic rule system. Then, for every sentence </> G f]E(< ty N >)> there exists an exponential time standard common derivation d^ that generates </> in every extension of < U,N >. Proof: We use the same definition for the standard common derivation as in Theorem 3.1.24. Since the rule system is highly exponential time, we have that the set of minimal proof schemes, Dr^ may be computed in exponential time. Once this is done, we need only to list the last rule in each proof scheme and construct the common derivation. Since there are only finitely many proof schemes, the common derivation may be computed in exponential time, i.e., in the time required to compute the set of minimal proof schemes. Theorem 5.2.69 Let < U,N > be a highly computable active nonomonotonic rule system such that (f) appears in every extension of the system. If d/ is the standard common derivation for <j> in < U, N > , then < U, N U {d/} > is highly computable and active. 83 Proof: Suppose < U, N > is a highly computable active nonomonotonic rule system and <j> appears in every extension of the system. Let d^ 1 be the standard common derivation for 4> in < U, N > as previously defined, and consider the system < U, N U {d^} >. This system is active and locally finite by Theorem 3.1.26. To show that it is highly computable we have left to show that it is computable, and that there exists an effective procedure which given any sentence ^ G U produces the set Dr^ of minimal proof schemes for tp. The set U has not changed since we have added no new sentences to the system by the addition of the common derivation. Thus, U is still computable. Since the set N is computable, and the common derivation is computable, we have that the set N U {d/} is computable. Thus, the system < £/, TV U {d/} > is computable. Since the original system < U, N > is highly computable we have that there exists an effective procedure which given any sentence € U produces the set Dr^ of minimal proof schemes for tp. This procedure is still effective upon the addition of the common derivation to the set of nonmonotonic rules of the system. Thus the new system < U, N U {d/} > is highly computable and active. Lastly, we find the following results as to the computability of the common derivations di((f>) and d 2 ((f>). Theorem 5.2.70 Let < U,N > be a highly computable nonmonotonic rule system. Then, for every sentence <j> G f)E(< U, N >), the common derivations di(4>) and ^2(0) for 4> are computable. Proof: The definition of each rule yields an algorithm for constructing it. Since the system < U, N > is computable we have that each of U and N is computable so that the set of minimal proof schemes, Dr,p, which is finite for any sentence ip G U, is computable. Since these rules are constructed from the last rule in each proof scheme, we have that they are computable. 84 Theorem 5.2.71 Let < U,N > be a highly exponential time nonmonotonic rule system. Then, for every sentence <f> e f] E{< U, N >), the common derivations d x (0) and ^(0) for <j> are exponential time. Proof: Since the rule system is highly exponential time, we have that the set of minimal proof schemes, Dr^ may be computed in exponential time. Once this is done, we need only to list the last rule in each proof scheme and construct the rules di((j)) and d 2 {(j>). Since there are only finitely many proof schemes, the rules may be computed in exponential time, i.e., in the time required to compute the set of minimal proof schemes. Theorem 5.2.72 Let < U,N > be a highly computable active nonomonotonic rule system such that (f> appears in every extension of the system. If d\ ((f)) is the common derivation for (j) in < U, N >, then < U,N U {d x {<f>)} > is highly computable and active. Proof: Suppose < U, N > is a highly computable active nonomonotonic rule system and appears in every extension of the system. Let d\(<j>) be the common derivation for in < U,N > as previously defined, and consider the system < U,NU {di{4>)} >. This system is active and locally finite by Theorem 3.1.26. To show that it is highly computable we have left to show that it is computable, and that there exists an effective procedure which given any sentence ip G U produces the set Dr,p of minimal proof schemes for xp. The set U has not changed since we have added no new sentences to the system by the addition of the common derivation. Thus, U is still computable. Since the set iV is computable, and the common derivation is computable, we have that the set TV U (di(#)} is computable. Thus, the system <U,NU {di(<j))} > is computable. Since the original system < U, N > is highly computable we have that there exists an effective procedure which given any sentence 85 ipeU produces the set Dr^ of minimal proof schemes for ip. This procedure is still effective upon the addition of the common derivation to the set of nonmonotonic rules of the system. Thus the new system <U,NU {di(#} > is highly computable and active. CHAPTER 6 ALTERNATE FORMALISMS OF NONMONOTONIC LOGIC In this chapter we will discuss how the results of the previous chapters trans- late into two particular formalisms of nonmonotonic reasoning, specifically Default Logic and Logic Programming. We will treat each separately, begining with the nec- essary definitions and preliminary theorems. Continuing, we show how each theory is equivalent to nonmonotonic rule systems. Finally we will see how some of the results of the previous chapters look through the eyes of these formalisms. 6.1 Default Logic: Preliminary Definitions and Theorems Definition 6.1.73 A DEFAULT THEORY is a pair (D,W), where W is a set of formulas of the language L, and D is a set of DEFA ULTS of the form d — A : Bi,...B n /C where A, Bi,...,B n , and C are all formulas of the language L and the default is interpreted as saying, "If A is true and B x , ..., B n are not contradicted, then conclude C." Call A the PREREQUISITE of d, and write p(d) = ,4. Call B x ,...,B n the JUSTIFICATIONS of d, and write J(d) = {B u ...B n }. Lastly, call C the CONSEQUENT of d, and write c(d) = C. Note that it is possible for a default to have no prerequisite and/or no justifications. If E is a set of formulas of the language L, let Cn(E) denote the closure of E under semantical censequence. Now, if (D, W) is a default theory, and S is a set of formulas of the language, call a default d GENERATING FOR THE CONTEXT S if p{d) is in S, and for all (3 e J(d), -1/8 £ S. Let GD(D, S) be the set of all defaults in D that generate for the context S. 86 87 Most simply, an EXTENSION, S, of a default theory (D, W) is a set of for- mulas of the language L that is the smallest set T (by inclusion) such that T is theoretically closed, i.e., T = Cn(T), T contains W, and for all defaults deD such that p(d) 6 T and V/? € J(d), -i0 g S, c(d) e T [BDK97J. This last property is best described as being "closed under the defaults of D." Example 6.1.21 Let a, b, and c be atoms in the language L and let D = {: {a}/b,: {c}/b,: {a}/^c,: {c}/^a}. Then the default theory (D, 0) has two extensions: S 1 =Cn({b,^c}) and S 2 = Cn({b,^a}). Moreover, we find that GD(D,S l ) = {:{a}/b,:{a}hc} and GD(D,S 2 ) = {:{c}/b,:{c}/^a}. Definition 6.1.74 Now, we may well-order the defaults of a default theory (D,W) by some well- ordering <. We may then define AD± to be the set of all defaults in D which are applied when the well- ordering is used to close W under the set of defaults. This is done in the following way: we define an ordinal n < . For every e < n^ we define a set of defaults AD, and a default d e . If the sets AD e ,e < a, have been defined but r/x has not been defined, then 88 (1) If there is no default d E D\ \J £<a AD e such that: (a) W U c(U,<o AD t ) h p(d) (b) W U c((J e<Q AD e ) \f -■/?, for every <= J(d) then rj^ = a. (2) Otherwise, define d a to be the <-least such default de D\ (J e<Q AD £ Then set AD Q = (\J £<a AD £ ) U {d a }. (3) Put AD±=\J e<1hi AD t . Intuitively, we begin with the set W of formulas, and apply the defaults of D in their order. Each time we apply only the ordering-least default which can be applied. At some point (since the ordinal is well-defined [MT93]) there will be no available dafaults that may be applied. At this point, AD± is the set of all defaults applied and n^ is the number of steps needed to reach this stopping point. Then, let T< be Cn(W U c{AD^)). This is the theory GENERATED BY < Then, GD(D,T±) C AD± [MT93] so that Cn{W U c(GD{D,T±))) C TV Now, if< is a well-ordering of the defaults and for every (5 in J(AD^), ->/3 $ Cn(WU c(AD^)) then T± is an extension of (D,W) [MT93]. That is, if AD± = GD(D,T^), then 2V = Cn(W U c(AD.<)) is an extension of(D,W). More precisely, ifT± = Cn(W Uc(GD{D,T±))), then T < is an extension of (D, W). We now have that (a) If S is an extension of (D, W) then there is some well ordering < of the defaults in D such that S = Cn(W U c(AD±)) = Cn(W U c(GD(D,S))) [MT93J. And, 89 (b) IfS = T± = Cn(W U c(AD±)) = Cn{W U c(GD(D, S))) for some well- ordering :<, then S is an extension of (D, W). Thus, S is an extension of (D, W) if and only if S = Cn{W U c(GD(D, S))). Let £(£>,w) be the set of all extensions of the default theory (D, W). Call two default theories {D u W x ) and (D 2 , W 2 ) EQUIVALENT, written (D u W x ) = (D 2 , W 2 ), if they have exactly the same extensions, i.e., ifE(Dt,Wi) = ^(d 2 ,w 2 )- Example 6.1.22 Let (D,W) be a default theory where D = {: /a -> 6} and W = {a}. Then consider the default theory (£>', 0) where D' = {: /a -> b,: /a}. These two theories are equivalent as they each have the same single extension S = Cn({a^b,a}). Theorem 6.1.75 (MT93) Let S C L. Then, S is an extension of (D,W) if and only if S is an extension of (D U D , 0), where D = {: /^ g W}. Proof : Suppose S is an extension of (D, W). Then, S = Cn{WL)c(GD(D,S))) which is clearly equal to Cn(0 U c(GD(D U D , S))) since each new default m D will generate for any context S. Thus, each extension of (D, W) is an extension of (DUD o ,0). For the same reasons, the converse also holds. Since they have exactly the same extensions, the theories are equivalent. Theorem 6.1.76 (MT93) Let S and S' be be two extensions for the default theory (b, W). Then, ifSC S', then S = S'. Theorem 6.1.77 (MT93) A default theory (D, W) has an inconsistent extension if and only if Sent(L) is an extension and (D, W) has no other extensions. 90 !^2 Equivalence of Default Logic to Nonmonotonic Rule Systems The equivalence of Default Logic to Nonmonotonic Rule Systems has been shown by Cenzer, Marek, Nerode, Remmel [1999] and others. Here, we give the equivalence as shown by Cenzer and Remmel. Let C be the prepositional language underlying the given default logic. With C fixed, all our nonmonotonic rule systems will have the same universe, namely the set of all well-formed formulas of C. We now show how to interpret a given default theory as a nonmonotonic rule system. Let (D, W) be a default theory. For every default rule r, a: ft,..., ft r = 7 construct the following nonmonotonic rule d r . __ a : -"A,.. .,-■& 7 Next, for every formula ip e £, define the rule d^ = — i> and for all pairs of formulas Xi»Xa define Xl.Xl => X2 ■ m Pxux2 = X2 Now define the set of rules N DfW as follows: N D ,w = {d r :r e D} U {d^ : ip e W or ip is a tautology} U {mp XuX2 : X u X2 € £}. We have the following result: Theorem 6.2.78 [MNR90] Let (D, W) be a default theory. Then a set of formulas S is a default extension of (D, W) if and only if S is an extension of nonmonotonic rule system (U,N DfW ). Theorem 6.2.78 says that at a cost of a simple syntactic transformation and additional encoding of logic as (monotonic) rules, we can faithfully represent default logics by means of nonmonotonic rule systems. 91 6.3 Previous Results Through the Eves of Default Logic We will consider only those deafult theories which have at least one, but only finitely many extensions. We will consider both the classical case and the constructive case. We consider a single default theory (D, W) that has a finite number of ex- tensions and where D and W are at most countable sets. We intend to explore the following question: If & is a formula of the language L, such that <f> € S for every extension S of (D,W), then what, if anything, can be said about the theory and/or the formula and its derivation in each extension. Let D be the set {: /?/# e W}. Let D x = D Li D . We consider now the default theory (A,0). This theory is equivalent to the original theory (D, W) since they have the same set of extensions. Theorem 6.3.79 For any formula <j> of the language L such that (f> 6 f| E (D,w), has a common derivation d 1 ^ which generates 4> in each extension S of (D, W). Proof: We prove the theorem using the equivalent default theory (£>i,0). Then, since (D, W) and (A,0) have the same extensions, the theorem holds for (£>, W). Suppose that is a formula of the language L such that 4> e f| s (£>i,fl)- Then G 5 for every extension S of (D x ,0). Since each extension S is of the form Cn(c(GD(D u S))), there must be, for each S, a finite set of defaults {d s u ..., d s n } C D 1 such that {cid'i), ..., c(d° n )} h <f>. Define d iM by i i i Where we simply omit from the prerequisite conjunction those i for which d s t has no prerequisite. Claim 1: For any extension S of (A, 0), d {M € GD{D X U {d (0 , s) }, S) 92 Proof of claim 1: Let S be an extension of (A, 0). Consider d (0>g) as denned above. Clearly d (0)4) £ JtyU^d^)}. Also,p(d (<M ) = AiPKi) G S since each p(d s ,) is in S since each d s { must be applied to deduce <\> and therefore each d\ is in GD(D X , S). Now, for every (3 in J(d {M ) = (J, J(d s l ), -i0 £ 5 since no /? in any of the J{d\) is in 5. Thus, d (<M € GD(D X U {d (<M },S). Moreover, c(d (0 , s) ) = A*^,) deduces <j> since {c(d*i), ..., c(d s n )} h 0. Thus, d { ^ } deduces in 5. Now we have for each extension S of (A,0) a default d ( ^ s) which deduces in 5. For any sets of formulas J u ...,J m define J x V...VJ m to be the set of disjunctions {iiV...Vj m : jj £ J u i = l,...,m}. We then define d 1 ^ to be k k k V i=1 ?(<W : V i=1 J (^.))/V t=1 c (° ? (M)> where S 1} ...,S* are all the extensions of the default theory (D, W). Call d ! the COMMON DERIVATION of in (£>i,0). Claim 2: d\ £ GD{D X U {d 1 ^}, S) for every extension 5 of (A, 0). Proof of claim 2: Suppose that is a formula of the language such that <j> £ n s (»i,0)- Consider d 1 ^ as defined above. Clearly d\ £ D x U {d 1 ^}. Also, for any extension S t of {D u fy, for all /3 in J{d ( ^ Si) ), -i/8 £ $ so that for every /? 6 J(d : ), /? = iiV...Vj* where j, € •/(<*(*,*)) for each i = l,...,jfe. Then, for any extension $ of (A,0), -<0 € 5 t if and only if ->jiA.../\->j k £ Si, which implies that -ijy € $, a contradiction. Thus, -.0 £ 5 for any extension S of (A,0). Lastly, p(d 1 ) 6 S for any extension S of (A,0) since for any S, p{d (M ) £ S and p(dV) = \J s p{d {4> , s) ) . Thus, (P 4 £ GD(D X U K },S) for every extension S of (£>i,0). Furthermore, c(d^) = V s c(d(0 ia) ) deduces in every extension 5 since each c(d (0)S) ) deduces 4> in 5. Thus, for any formula of the language such that <f> £ f) E (Dl , 0) , has a common derivation d 1 ^ which generates in each extension 5 of (A,0). Note that d 1 ^ may be in D x , but then (D x u{d^},0) will have the same set of extensions as (D U Q), i.e. (L>i U (d^},0) will be equivalent to (£>i,0). Further note that since d 1 ^ generates 93 for each extension S of (A,0), we have that it generates for the intersection of all the extensions, that is, it generates for p|£(z>,w)- This completes the proof of Claim 2 and thus of the theorem. Theorem 6.3.80 For any formula <j) of the language such that e f)T,( D}W) , define d*^ to be VMm) : U J (^))/ V c (<w- s s s Then, iff 6 GD(A U K }>n*W))- Proof : Again, we prove the theorem using the equivalent default theory (£>i,0). Since (D, W) and (2?i,0) have the same extensions, the theorem holds for (D, W). Let be a formula of the language such that <f) <E f|^(Di,0)- Consider d% as defined above. Clearly d% e D x U {cf%}. Now, for every extension 5 in E (Dl)0) we have that d {M generates for S so that p(d (<M ) e S. Thus, p(d\) = \J s p(d {M ) € fl s (£»i,0)- Lastly, for every extension 5 in E (£ , li0) we have that V/3 6 J(d {M ), ->/3 $ S. Now, V/? € /(d%) = |J s J{d {4> , s )),Pe J(d {M ) for some extension 5 so that -./? £ 5. Hence, -i/3 £ n s (0i,0)- Th us d% generates for f|S(D,,0). Note that although this new default generates for the intersection of all the extensions, it may not generate for each particular extension. Example 6.3.23 Consider the default theory (D,0) where D = {:{^a}/b,:hb}/a}. This default theory has two extensions, Si = Cn({b}), and S 2 = Cn{{a}). 94 We have that the formula a V b is in both of the extensions and we find that d* a vb -■ {-a,^6}/aV6. By the theorem, d* aX ,b generates for the intersection of the two extensions. However, it does not generate for either of the extensions Si or S 2 since b £ Si and a € S 2 , respectively. Since there are only a finite number of d\, there are only a finite number of possible prerequisites, sets of justifications, and consequents of d^ s ). Thus there are only a finite number of possibilities for d^ tS ) for each extension. Because of this, and because we assume that the default theory has only finitely many extensions, we are not in danger of having an infinite disjunction or union in d 1 ^ or in d*^. Example 6.3.24 The common derivation of any formula (j) in (D, W) may not be found in D or in W as this example illustrates. Let a, b, c be atoms in the language and let D = {: {a}/b,: {c}/b,: {a}hc,: {c)ha}. Then the default theory (D, 0) has the two extensions Si=Cn({b^c}) and Also, as before, and S 2 = Cn({b,^a}). GD(D,Si) = {:{a)lb,:{a}hc} GD(D,S 2 ) = {:{c}/b,:{c}/^a}. 95 There is no default of D that derives b in both extensions. However, we may condsider the common derivation of b in (D, 0) which is d\ =: {a V c}/b V b =: {a V c}/b. Then, d 1 b will generate b in each of these extensions. Theorem 6.3.81 E( D ,w) C T,^ D u{d^},w) for any (j) 6 f| s (D,w)- Equivalently, E (Dl)0) C £(D 1 u{dM,0), f or an y $ e fl s (»i,0)- Proof : Suppose that i^ef) £(£>i,0) and suppose further that 5 is an extension of (A, 0)- Then, (j) € S = Cn(c(GD(D u S))). We want to show that 5 = Cn(c{GD(D 1 u {d 1 *}, 5))). Now, c(GD(D u S)) C ^(AuK^.S)). Thus, 5 = Cn(c(GD(A,5))) C Cn(c(GD(Di U {d^},S))). We will now show that c(GD{D l U {d 1 ,},^)) C 5 = CnWGDpx.S))). Let d 6 GD(D X U {d^.S). If d € A then d € GD{D U S) so that c(d) € Cn(c(GD(A,5))) = S. If d £ D 1? then d = d J so that c{d) = V s c K<m)- Now, d (<M generates for 5 so that c(d {<t>tS) ) e c(GD(D u S) and therefore c(d) = \/ c (<W eS = Cn{c(GD(D 1 ,S))). s Thus, c{GD{D l U {d%}, 5)) C 5 so that S = Cn{c{GD{D l U {d\}, S))). Thus, 5 is an extension of (D 1 U {d%},0), and E (Dl , 0) C E (DlU{d i 0}j0) . The converse of this theorem is false. As the next two examples show, the two default theories (D, W) and (Du {d 1 ^}, W) may be equivalent, but need not be. That is, we may have that E(d,W) = E(Du{#a),W), but this is not always so. 96 Example 6.3.25 Consider the default theory where W = and D = {: {a}/b, : {c}/b, : {a}/-ic, : {c}/->a}. 77izs de/au/^ i/ieory has two extensions: Si=Cn({6,-c}) and S 2 = Cn({b,^a}). We found previously that b is in each extension and that the common derivation of b in (D, 0) is d\ =: {a V c}/b V b =: {a V c}/6. 4<tttn£ tf»w new default to D, we see that (D U {d\}, 0) has the same extensions S { and S 2) since applying d\ does not prevent the application of any default in D. Example 6.3.26 Now consider the default theory (D, 0) where D = { Pl : / Cl ,p 2 : /c 2 , : {^a, -pi}/p 2 , : {-a, ^p 2 }/p u ■ hPi,^P2}/piVp2,Ci Vc 2 : {^Ci,-ic 2 }/a}. This theory has two extensions, S x = Cn({p 2 ,c 2 }), and S 2 = Cn{{p l ,c l }). The formula c x V c 2 is in each extension and we find that rf (ciVc 2 ,si) =P2 : /c 2 , and 97 so that d\ivc 2 = Pi Vp 2 : /d Vc 2 . 77ien, Si andS 2 are both extensions of (DU {d l ClVC2 },®), but this default theory will have a third extension S 3 = Cn({p x V pa, d V c 2 , a}), w/nc/i m noi an extension of the original default theory (£>,0). In the previous example, S 3 is the only new extension obtained by adding the common derivation to the set of defaults. To see this, let S be any new extension. The common derivation must generate for S, else S is an extension of the original system. Thus, we have that p, Vp 2 € S so that the conclusion c x V c 2 is in S as well. If pi € S, then c : 6 S by the default p l : /c x so that Si C S, a contradiction to the noninclusive property of extensions, since S is not an extension of the original system. Similarly, if p 2 e S, then c 2 e S so that S 2 C S, a contradiction. Thus, neither of pi or p 2 is in S. Also, if a is not in S, then the rule : {--a, ^p 2 }/pi applies to conclude p, in S. Thus, ae5. From this we now have that S 3 C S so that S 3 = S since extensions are noninclusive. Thus, there is only the one new extension. Suppose we let I x be the intersection of all the extensions of the original default theory (D,0). Then, /i = Cn({(p 2 Ac 2 )V(p 1 Acj)}). We consider the new dafault theory (D 2 ,<b) = (Du{d\ lVC2 },$) and the set I 2 of all conclusions common to every extension of (D 2 ,0). We find that h = Cn{{( Pl V pa) A ( Cl V c 2 )}) C I x . 98 Moreover, we could choose a conclusion common to all the extensions of (£) 2 ,0), such as p\ Vp 2 . This has the common derivation rf2 piv P2 == I" 1 ** V -ipi, ->a V -<p 2 , ->a, -ip x V ->p 2 }/Pi V p 2 . In any new extension S of £>3 = (D 2 u{d 2 plVp2 },0) that was not an extension of the theory (D 2 , 0), this common derivation must apply. Similarly to the previous arguement, none of pi,p 2 ,c t or c 2 can be in S else we contradict the noninclusive property of extensions. p\ V p 2 must be in S since the common derivation applies. Thus, by the common derivation for C\ Vc 2 , we conclude c\ V c 2 in 5 and thus a is in S by the appropriate rule from D. This is a contradiction since the common derivation requires that a not be in S. Thus, there are no new extensions, that is, (Z) 2 ,0) has the same set of extensions as (D 3 ,0). On a different note, we may force the intersections I x and I 2 to be equal by taking <p to be /\i\. This appears in every extension of (D,0). Letting D 2 = (DLl{d 1 4> },®) We find that if S is any new extension, then (j) € S since the common derivation must apply (else S is not new). Thus, h c h = h n S C /j so that I\ = I 2 . If we have a formula <f> appearing in some but not all the extensions of (Di, 0), we may in the same fashion as Theorem 6.3.79 create a common derivation for that will generate in each extension of (A,0) in which it appears. However, we find that in this case Theorem 6.3.81 becomes false, as the next example illustrates. Example 6.3.27 Let (D, 0) be the default theory where D = {: {-iai, ->a 2 }/a 3 , : {-ia 2 , ->a s }/ai, : {-101, -ia 3 }/a 2 , Pi : {«l}/ci,Pa : {a 2 }/c 2 ,a 3 : /p, Vp 2 ,a! : /p u a 2 : /p 2 }. 21Wj £/ieon/ /ias as i/iree 0/ ate extensions, Si = Cn({a 3 ,p l Vp 2 }), 5 2 = ^({02,^2,^}), and 53 = CndaxiPua}). We see that the formula c x V c 2 is in both S 2 and S 3 , but is not in Si. We find the standard common derivation for c\ V c 2 to be d l Cl vc 2 = Pi V p 2 : {ai V a 2 }/ci V c 2 . ,4ddma this new default to the set of defaults D, we find that both S 2 and S 3 are extensions of the new default theory {D U {d\ lVC2 }, 0). S u however, is not an exten- sion of (D U {d^jvcJJ) since it is no longer closed under the set of defaults. It is important to note that 5 X is a subset of{a 3 , Pl Vp 2 , Cl Vc 2 } which is an extension of (DUK C1VC2 },0). Theorem 6.3.82 Let (£>i,0) be a default theory such that appears in some but not all of the extensions. Consider d x to be the common derivation of (j> as defined m Theorem 6.3.79. Then, for any extension S of {D u $), there is an extension S of (A U {a%},0) such that S C 5. More specifically, if <f> e S then S = S and if (j) £ S then S is strictly contained in S. 100 Proof: Suppose that (£>i,0) is a default theory such that tf> appears in at least one, but not all of the extensions. Consider d x ^ to be the common derivation of <\> as defined in Theorem 6.3.79. If <fi appears in only one of the extensions of (A, 0), then the common derivation d 1 ^ is found in D x so that (D x , 0) = (D x U {d l <p}, 0), and the theorem is trivially true. Thus, suppose that <j> appears in al least two exensions of the default theory (Dj,0), but does not appear in every extension. Let S be an extension of (£>i,0). If S is an extension of the new system (D x U {d 1 ^,®), we are done. Also, if (j> is in S, then 5 is an extension of (D x U {d 1 ^},®) by the proof of Theorem 6.3.81. Hence, consider the case in which <j> ^ S, and S is not an extension of the new system (Di U {d 1 ^},©). Since S is an extension of (£>i,0), we have that S = Cn(c(GD(D u S))). If d 1 ^ does not generate for S, then GD(D l u{d 1 )P },S) = GD(D u S) so that S = Cn(c(GD{D l U{d l 4> },S))) and thus S is an extension of the new system (D x U {d 1 ^}, 0), a contradiction. Thus, d 1 ^ generates for S so that <t> = c{d\) e c{GD{D l \J {d 1 ^}^)). Let S x =Cn(Su{d\}))). Then, Si = Cn{c{GD{D l U {d\},S))) = Cn(c(GD(D 1 u{d\},S 1 ). Thus, Si is an extension of the new system (D x U (d l *},0) and clearly S is strictly contained in Si. Thus, if S is an extension of (£>i,0) then either S is an extension 101 of (Di U {d 1 ^},®) (in the case of <j) belonging to S) or S is strictly contained in an extension of (Di U {d 1 ^},©) (in the case of not belonging to S). Refering to example 6.3.26 we may consider any default theory (D, W), the equivalent default theory (£>i,0) and the set h =P|E (Dli0) . Differently now, for every <f> in this set, we can find a common derivation d 1 ^ which generates <f> in each extension S of {D u 0). Consider the default theory (D 2 , 0) defined by (AU{d%|0€/i},0). We may then repeat the procedure to find h = (|£(D 2 ,0), and if this set is not empty, then we can find common derivations d% for each </> in I 2 such that d 2 ^ generates in every extension S of (D 2 , 0). Then, we may condsider the default theory (.03,0) defined by (£> 2 u{d%|0e/ 2 },0). We continue this construction by, assuming that D n is defined, let In = £(D n ,0)- Then, letting d% be the common derivation for <j> 6 I n in (D n , 0), we define D n+1 to be (I> B U{d%|*€/„},0). This may be continued until 7 fc is empty for some k and/or D k = D t for all / > k for some fc. This inductive definition begs the following questions. Is there a limit to this process, i.e., is there always some k for which I k is empty and/or D k = D t for 102 all / > k? Does it make a difference if we work in the case where D and W are finite versus countably or uncountably infinite? These questions should be investigated. Example 6.3.28 Consider the first default theory of this section. Using this default theory, we would find D 2 to be D U {d\} = {: {a}/b, : {c}/b, : {a}/-*, : {c} ha, : {a V c}/b}. {D 2 ,0) has the same extensions as (D, 0) so that I 2 = h = {b} and d 2 b = d l b . Then Dk = D 2 for all k > 1. Remark 6.3.83 By Theorem 6.3.81, we have thafL( Dl #) C S (D2i 0) C ... C S( Dn ,0) C S(D n+1 ,0) Q .... For a finite language, or just a finite i\, we must eventually have /„+] = /„ for some n. At this point, we find that we will have a common derivation in D n for each <A € /„, when we consider D n to be defined using all of the common derivations for conclusions in /„_!. (£>„,0) will be said to HAVE common derivations. Theorem 6.3.84 For any default theory (£>,0) with finite I\ } there exists an n such that (£> n ,0) has common derivations, and the default theory D n is equivalent to the default theory D n+ k for any k. For an alternate approach, we might consider the default theory (A,0) and the set ii as before. However, we may choose one element from I x and define D 2 to be the default theory (Au{dV},0) as seen for Example 6.3.26. We may then consider the set of all formulas which appear in every extension of D 2 , choose some ip among those, and define D 3 to be (D 2 U{rf%},0). 103 We may continue in this way, however, we will keep with the previous construction. Using either construction, and considering the language to be infinite, we still have that I x D I 3 D /$ D.... We may define I* to be the intersection of all the /„, define D* to be the union of all the D n , and define E* to be the union of all the sets of extensions of the default theories (Z) n ,0). We then find the following: Theorem 6.3.85 /• = f|E* Proof: Suppose that <j> G I*. Then, 4> g I n for all n so that e f|E (Dn , 0) for all n. Letting S be any extension in E* we have that S is an extension of (£>„, 0) for some n so that <j> e S and thus e f)E*. For the reverse containment, suppose that we have <j) € f] s *- Then, (f> e S for any extension S e E* so that $ € 5 for any extension S of any (D n , 0). Hence, <£ € I n for any n so that (f>ef]I n = r. Thus the equality holds. Theorem 6.3.86 E* C E (D . )0) . Proof: Let 5 6 E* so that 5 is an extension of some (D„,0) and an extension of any (D m , 0) for m > n. We want to show that 5 is an extension of (D*, 0). To do this, suppose that a default d G D* generates for S. d G D m for some m, and hence for some m > n. Since S is an extension of (D m , 0) we have that the consequence of d is in S so that S is an extension of (D*, 0). It is known that the extensions of a default theory form an antichain. That is, if Si C S 2 where 5 X and 5 2 are extensions of the same default theory (D, 0), then Si = S3. Thus, the extensions of (D, 0), whether or not we take the constructive view, form an antichain so that, assuming they are distinct, no one extension is contained in any other extension. The following results are of general interest. 104 Theorem 6.3.87 f\E {Dt9) D Cn(f[ s (c{GD{D,S)))). Proof : For every extension S of (D, 0), f]c(GD(D,S)) C c{GD{D,S)) C Cn(c(GD(D,S))) = S s so that f\ s c(GD(D, S)) C S. Thus, since each 5 € £(d,0) is a theory, we have that f|£(D,0) is a theory so that Cn(f] s (c{GD(D,S)))) C f| E (D,0)- Theorem 6.3.88 Cn(C\ s (c{GD{D,S)))) C Cn(c(GD(2), f| £(!>,»))) and tfiej, are eaua/ »/ and only if f] £(d,0) = 5 /or a// extensions S, or Vd € GD(D,n E (^))' V ^ € J(d),-,/? £ |J E (^)- Proof: Let c(d) G fls^CD^, S))). Then, d G GD(D,S) for every ex- tension 5 of (£>,0). Thus, for every extension 5, we have that p(d) G 5 and V/3 G J(d),^(3 i S. So, p(d) G nS(D,e) and V/3 G J(d),-./? £ f|V»)' Th us, dG G*D(D,flE(D,0)) so that c{d) G c(GD(D,ri£(o,0)))- Hence, n(c(GD(D,5))) C c(GD(D,f|E (Di0) )) 5 so that Cn(f](c(GD(D,S)))) C Cn(c(GD(D,f|E (D , 0) ))). s Now suppose that c(d) G c(G'D(D,nE (D)0) )). Then, d G GD(D,nS (Di0) ) so that p(d) G D s (d,0) and V/? G J(d), -./? £ D 2 (d,0))- This means that p(d) G 5 for every extension 5, but we do not necessarily have that V/3 G J{d),^/3 ^ (JE (Dj0) , the necessary condition if we are to have that c(d) G DsW^tA S))). Now, if either fl £-(£>,0) = 5 1 for all extensions 5, or Vd G GD(£>,p|E Pi0) ),V/? G J(d),^3 £ U E W0)' 105 then then we would have that c(d) 6 f\ s (c(GD(D, S))). Then, c(GD(D, f|S(D,0))) C f\(c(GD(D,S))) s so that Cn(f](c(GD(D,S)))) = Cn(c(GD(D, f]j^, m ))). s Clearly, if Cn(f] s (c(GD(D, S)))) = Cn(c(GD(D, fl^W)), then either ft E (D , 0) = 5 for all extensions S, or Vd € G-D(£>,n s (^))> V /? 6 .7(d), -0 £ |J E (^)- Example 6.3.29 Let D = {: /p,p : {a}/e,p : {^a}/-a}. 77jen, (fee de/aw/£ i/ieory (D, 0) /ms i/ie extensions and so that and Then, but S l =Cn({p,e}) S 2 = Cn({p, -na}) GD(A5 1 ) = {:/p > p:{a}/c} GD(D,5 2 ) = {:/p,p:{^ a }/-a}. GD(D,S l )nGD(D,S 2 ) = {: /p], GD(D, Si n 5 2 ) = G£>(D, {p}) = D since p e {p} and neither -.e nor a is in {p}. We then see that c(GD(D, 50) n c(GD(D, S 2 )) = {p} ± {p, e , ^ a } = c(GD(D, 5, n 5 2 )). 106 Hence, Cn(c(GD(D, 50) n c(GD{D, S 2 ))) = Cn({p}) ? Cn(c(GD(D, S 1 nS 2 ))) = Cn({p, e, -a}). Corollary 6.3.89 Cn(f) s (c(GD(D,S)))) = Cn(c(GD(D,f]i: {D ^))) ,i/(£>,0) is a justification free default theory. Proof : Suppose (Z>,0) is a justification-free default theory. Then, the stan- dardized theory {D, 0) is also justification-free. Then, W € GD(D,p|£ (i) , 0) ),V/? 6 /(d), ^3 £ |JE (D , 0) since there does not exist /? G J(d). Thus, Cn(f|(c(GD(D,5)))) = Cn(c(GD(D,f|E {/3 , 0) ))). s Note that a justification-free default theory is monotone, but the nature of the result is still interesting. We now take the case of constructive default theories. Again, consider a single default theory (D, W) where D and W are at most countable sets. In this section, we consider the same question about default theories as previously, but use an constructive approach. That is, we consider that pVq is not derived unless one of p or q is derived. Before considering the theory as is, we first "standardize" the theory as we did previously to a more suitable one (£>i,0). This is done in the following way: Let D be the set {: /V# e W}. We consider now the default theory (D x , 0) Where D x = D U D . This theory is equivalent to the original theory (D, W) since they have the same set of extensions [MT93]. 107 Again, we consider 0, a formula of the language L such that € fl^Di,!). Then e S for every extension S of (A,0)- Since each extension S is of the form Cn{c{GD(D u S))), there must be, for each S, a finite set of defaults {d s x , ..., d s n ] C Di such that {c^), ..., c(d s n )} h 0, as before. The advantage of the constructive approach is that it allows us to view each set of justifications as a single formula instead of as a set of formulas. Then, instead of asking if each element of the set of justifications is not contradicted in a context, we would ask if the justification itself is not contradicted in the context. As it stands, each default d s t has as its justifications the set {/3\, ...,^ k } for some ff i i formulas of the language. We may instead let J(d s i) = 0\A ... A/?Y Then ^J(d°i) = -./^ v ... v-./3\ is in the extension S if and only if -./^ g S for some j, a contradiction since each d s { generates for S. Thus, we have that for each extension S, -. J(d s l ) <£ S for each *. We find that several of the theorems of the last section still hold. Theorem 6.3.90 For any formula (f) of the language L such that 6 f]T, (DM1 , has a common derivation d 1 ^ which generates in each extension S of(D,W). Proof : We prove the theorem as before using the equivalent default theory (£>i, 0)- Then, since {D, W) and (A, 0) have the same extensions, the theorem holds for (D, W). Suppose that is a formula of the language L such that 6 n s (o,,0). Then there must be, for each extension S, a finite set of defaults {d s x , ..., d s n } C D x such that {c(d\), .., c(d s n )} h 0. Define e/ (<M by t i i Claim 1: For any extension S of (£>i,0), d {M e GD(D X U {d i</>tS) } , S) Proof of claim 1: Let S be an extension of [D u $). Consider d {M as defined above. Clearly d {M € D x U {d (0!i) }. Also, p(d {4> , s) ) = AiP(rf'i) € 5 since 108 each p(d s i) is in S since each d s { must be applied to deduce <j> and therefore each d\ is in GD{D U S). Now, for this extension S of {D u 0), -J(d (<M ) = -.(/^ J(rf s 2 )) g 5 if and only if Vj^-A^i)) € 5. Because of the constructive view we are taking, this cannot happen unless ^J(d s i) G S for some i, a contradiction since -^J{d s i) <£ S for each i. Thus, ->J{d {M ) £ 5. So, d {M G ££>(£>! U {d (0 , a) },S). Moreover, c(d (<M ) = Ai c ( rfs i) deduces since {c^), ..., c(d s n )} h 0. Thus, d (0ii) deduces in 5. Now we have, as in the last section, for each extension S of {D u 0) a default rf(0 )S ) which deduces in 5. Define rf 1 ^ to be V r p(d(*,«)) = V ' J{d {M )l\lc(d ( ^ s) ). s s s Call d 1 * the COMMON DERIVATION of in (A,0). Claim 2: d% G G?D(A U {d%}, 5) for every extension 5 of (A, 0). Proof of claim 2: Suppose that is a formula of the language such that <j> G fl s (£>i,0)- Consider d 1 ^ as defined above. Clearly d 1 ^ G D x U {d 1 ^}. Also, for any extension S of (A,0), -J(dV) = - V, M<m) 6 5 o if and only if f\ s {^J(d iM )) £ S . However, this is if and only tf->J(dfa ao) ) G S , a contradiciton. Thus, ^J(rf ! ) f| 5 for any extension 5. Lastly, p(d x ) G 5 for any extension S of (A,0) since for any 5, p(d (0i4) ) G 5 and p(d%) = \J s p( d (*,*)) ■ Thus, d 1 * G GD{D l U {d^}^) for every extension 5 of (Di,0). Furthermore, c(g^) = V s c(d (<M ) deduces in every extension 5 since each c(d^ f8) ) deduces in 5. Thus, for any formula <j> of the language such that G fj^Di § has a common derivation d 1 ^ which generates in each extension 5 of (Z?i,0). Note that d 1 ^ may be in D u but then (D, U {d\, 0) will have the same family of extensions as (D u 0). Theorem 6.3.91 For any formula (j> of the language such that (/) G f\E( DtW ), define d% to 6e V>(<W : A a J(d iM )/\/ a c(d {M ). Then, <r*€GD(AU{d%},f|E (iW ). 109 Proof : Again, we prove the theorem using the equivalent default theory [Di,$). Since (D,W) and (A,0) have the same extensions, the theorem holds for (D, W). Let be a formula of the language such that (j> G f| s (Di,0)- Consider d* as defined above. Clearly d% £ D x U {d%}. Now, for every extension 5 in E tDl>0) we have that d (0>4) generates for S so that p(d (0>s) ) e S. Thus, p(d%) = V s p{d {4><s) ) S D s (Di,0)- Lastly, we have that -«J(d%) = ^ f\ s J{d {4>>s) ) € f| E (D,vv) if and only if V s h J ( d (4>,s))) 6 HW)' However, this is if and only if -nJ(d {<f> , So) ) 6 f|£(/W) for some extension 5 . Then, ^J(d (( ^ o) ) e S , a contradiction. So we have that -"•/(d**) ^ n s (o,w)- Thus d* generates for f| s (Oi,fl)- Moreover, cid*^ = c^) generates <j) in every extension so that c(d* c/> ) generates <j> in f\E(D,wy As before, since there are only a finite number of d s h there are only a finite number of possible prerequisites, sets of justifications, and consequents of d ((M) . Thus there are only a finite number of possibilities for d (<M . Because of this, we are not in danger of having an infinite disjunction or conjunction in d 1 ^ or in d%. Example 6.3.30 Consider the first default theory of this section. Under this ap- proach, we let D - {: a/b, : c/b, : a/->c, : c/->a}. Then the default theory (D, 0) has the two extensions and Also, and Si=Cn({6,^c}) S 2 = Cn({b,^a}). GD(D, S^ = {: a/b, : a/^c} GD(D,S 2 ) = {:c/b,:c/^a}. 110 Just as before, there is no default of D that derives b in both extensions. However, we may condsider the common derivation of b in (D, 0) by the methods of this section, which is d\ =: a V c/b V b =: a V c/b. Then, d l b will generate b in each of these extensions. Compare this version of the common derivation of b in (D, 0) to that of the previous section where we had d\ =: {a V c]/b V b =: {a V c]/b. We see that the two methods produce very similar results, but that the common deriva- tion produced by the constructive methods of this section is computationally simpler. By the same arguement as in Theorem 6.3.81, we still have that E (D ,w) C £(DuK },ty) for any (j> £ f\T, {DiW) . Equivalently, E (Cl , 0) C E (DlU{d i 0}0) , for any <j) G plE( £ , l! 0). Also as before, the converse of this theorem is false. We may again inductively define the default theory (£> n ,0) as we did in the last section. Investigations into the questions raised by this definition are further warented in this setting as the common derivations are computationally simpler and the constructive view may make the difference in what the answer to those questions will be. Example 6.3.31 Considering our basic default theory again, and the methods of this section, we would find D 2 to be A U {d\} = {: a/b, : c/b, : a/^c, : c/^a, : a V c/b}. Again, (D 2 , 0) has the same extensions as (D, 0) so that I 2 = I x = {b} and d 2 b = d\. Then D k = D 2 for all k > 1 . Ill Remark 6.3.92 As in the last section, we will have that 2(^,1) C £(/>,,!) C ... Q s (Dn!0) C E {Dn+li0) c .... When considering the finite constructive case, we may be sure that it is still interesting in the case of default logic by considering the two atom case as we did before. Here, there is a bit more to say. When considering a constructive view of the default theories, we must ask to what extent this view weakens the results. That is, by using a constructive view, what families of possible extensions are excluded and does this exclusion cause the subsequent theory to be uninteresting. In this section we examine the case where the language has two atoms, p and q. Any extension of a default theory must be a theory in the language. There are fifteen possible extensions which may be partially ordered by implication. They are: Cn(p A q), Cn{p A -. g ), Cn{^p A q), Cn{-^p A -.g), Cn(p), Cn{q), Cn(-p), Cn{^q), Cn(p <—> q), Cn{p ♦— > -, 9 ), Cn(pV q) , Cn(pV-^q), Cn(-<pVq), Cn(^pV Now, for any default theory we have that no one extension is contained in any other extension. This greatly limits the possible sets of extensions that any one default theory in this language can have. To see the possibilities more easily, we make the following definitions: A = {Cn(p V q), Cn(p V -.g), Cn{^p V q), Cn(^p V -- 9 )} B = {Cn(p), Cn(q), Cn(-ip), Cn(-qf), Cn(p ^-> q), Cn{p f— ► -, g )} C = {Cn{p A q), Cn(p A -.g), Cn{^p A q), Cn(^p A -q)} 112 Taking the constructive view, we cannot derive any element of A and we cannot derive either of Cn(p i — ► q) and Cn(p < — ► -<q). Without the constructive view, there are 141 possible families of extensions coming from: 15 subsets of A, 63 subsets of B, 15 subsets of C, 12 families having one element from A and one element from B, 6 families having two elements from A and one element from B, 12 families having one element from B and one element from C, 6 families having one element from B and two elements from C and 12 families having two elements from B and one element from C. Taking the constructive view, we eliminate all but 46 of these possible families of extensions. We allow only 15 of the subsets from B, all of the 15 subsets from C, 8 families having one element from B and one element from C, 4 families having one element from B and two elements from C, and 4 families having two elements from B and one element from C. We should note that any default theory whose family of extensions is a singleton is a monotone theory The resulting mathematics remains interesting as for any of the 46 possible sets of extensions we can find a default theory with exactly those extensions. Specifically, for any acceptable family F = {Cn(7\)„ ..., Cn(T n )}, the default theory (D, 0) where D = {= hW * i}/T t \l < i < n} will have F as its set of extensions. For example, for the family {Cn(p),Cn(q)} we would choose the default theory ({: ->g/p,:-np/g},0). This default theory will have exactly the two theories Cn(p) and Cn(q) as its exten- sions. Now, since the intersections of families of extensions is of particular interest, we might ask which acceptable families of extensions have intersections which yield a 113 specific theory. Knowing this, given a theory which we desire to see as the intersection of extensions we may create the default theory whose extensions intersect to yield that theory. In the two atom case, intersections of families of extensions proceed as follows: Cn(p A q), Cn(p A ->q), Cn(^p A q), and Cn(^p A -.<?) are the intersections of only themselves. The other ten theories (aside from Cn(true)) can be seen as intersections of the following families: Cn(p) = f]{Cn(p)} = f]{Cn(p A q),Cn(p A -<?)}, Cfl(-V) = f|{Cn(-p)} = f]{Cn(^p A q), Cn(^p A -,<?)}, Cn(q) = f]{Cn(q)} = p\{Cn(p A q), Cn(^p A q)}, CnH) = f]{Cn(^q)} = f]{Cn(p A -y), Cn(^p A -*)}, Cn{p < — > q) = f]{Cn(p A q), Cn{^p A ^q), Cn(p < — > ^q) = f]{Cn{p A - 9 ), Cn(-p A q)}, Cn(p Vq) = (~){Cn(p), Cn(q)} = f]{Cn(p A q), Cn{p A -.g), Cn(-* A 9)}, Cn(p V -g) = f|{Cn(p), Cn(-g)} = f|{Cn(p A q), Cn(p A -.9), Cr^-^ A -.?)}, Cn(-p V 9 ) = f|{Cn(-np), Cn(g)} = f|{Cn(p A ?), Cn(-p A q), Cn(-,p A -*)>, Cn(^p V -.9) = f|{Cn(-.p), Cn(-g)} = (~){Cn(p A -.g), Cn(^p A g), Cn(-*> A -*)}. So we see that any given theory may be derived as the intersection of a set of acceptable extensions. 114 6.4 Logic Programming: Preliminary Definitions and Theorems The stable model semantics of logic programs has been extensively studied. Unfortunately, the set of stable models of a recursive prepositional logic program with negation or even of a finite predicate logic program with negation can be quite be quite complex. For example, in [MNR90], it is shown that for any recursive propositional logic program P, there is an infinite branching recursive tree T P such that there is an effective 1:1 degree preserving correspondence between the set of stable models of P and the set of infinite paths through T P . In [MNR92a] it is shown that given any infinite branching recursive tree T, there exists a recursive propositional logic program P T such that there is an effective 1:1 correspondence between the set of infinite paths through T and the set of stable models of P. Moreover, in [MNR92a], it is shown that the same result holds if we replace recursive logic programs by finite predicate logic programs with negation. These results imply that the set of stable models of a recursive propositional logic program or a finite predicate logic program can be extremely complex. For example, it follows from these results that there a finite predicate logic program which has a stable model but has no stable model which is hyperarithmetic. The main motivation for this paper was to develop conditions on recursive logic programs P which would guarantee the existence of well behaved stable model for P, i.e. a stable model of P which is recursive or possibly even polynomial time. We shall now carefully define the notion of recursive logic programs. Then we shall define the notion of proof schemes which will lead to the definitions of locally finite programs. Finally we shall describe the extension of the Reiter's concept of normal default theories to recursive logic programs following Marek, Nerode and Remmel. A program clause is an expression of the form C = P<-gi,...,g n ,-T 1 ,...,-.r m (6.1) 115 where p,qi, . . . ,q n ,ri,. . . ,r m are atomic formulas in some propositional language C. A program is a set of clauses of the form (6.1). A clause C is called a Horn clause if m = 0. We let Horn(P) denote the set of all Horn clauses of P. H P is the Herbrand base of P, that is, the set of all atomic formulas of the language of P. If P is a program and M C H P is a subset of the Herbrand base, define operator T PM :V{H P ) -* V{H P ) where T PM {I) is the set of all p such that there exists a clause C = p «- ft,. . . ,^,-iTi -*•„, in P such that ft € /,. . . ,fc € / and {r lr ..,r m }nM = 0. The operator T P , M is a monotonic finitizable operator, see Apt (1990), and hence possesses a least fixpoint F PM . Given program P and M C # P , the Gelfond- Lifschitz reduct of P is defined as follows. For every clause C of P, execute the following operation: If some atom a belongs to M and its negation ->a appears in C, then eliminate C altogether. In the remaining clauses that have not been eliminated by the operation above, eliminate all the negated atoms. The resulting program P$ L is a Horn propositional program (possibly infinite). The program P$ L possesses a least Herbrand model. If that least model of P° L coincides with M, then M is called a stable model for P. Gelfond and Lifschitz (1998) proved the every stable model of P is a minimal model of P and that M is stable model of P iff M = F P<M . Having characterized stable models as fixpoints of (parametrized) operators, consider the form of elements of F PyM . A P, M- derivation of an atom p is a sequence (Pi, • • >tP$) such that (i) p s = p and (ii) for every i < s, either n p t «-" is a member of P or there is a clause C = " Pi <- ft, ...,«,, -*i,. .. , -r m " such that C G P, Qu---,q n 6 {Pii -.,ft-i} , and ri,..., r m £ M. It is easy to show that F PM is the set of all atoms possessing a P, M-derivation. Thus M is a stable model of the program P if and only if M consists exactly of those atoms which possess a P, M- derivation. 116 The property that a sequence (p l5 . . . ,p s ) is a P, M-derivation of an atom p does not depend on the whole set M but only on the intersection of M and a certain finite set of atoms that occur in the derivation. In order that the sequence (pi,...,p s ) be a P, M-derivation of an atom p s , some atoms must be left out of the set M. Each derivation depends on a finite number of such omitted atoms. In other words, if we classify the atoms according to whether they are "in" or "out" of M, the property that a sequence (pi,...,p,) is a P, M-derivation depends only on whether a finite number of elements are out of M. The notion of a proof scheme formalizes this idea. A (P-)proof scheme for an atom p is a sequence S = {(p u Ci,Ui)) s i=l of triples such that for each triple (p t , Q, U { ), p { E H P , d e P is a clause with the head p % and Ui is a finite subset of H P . Such sequence S is a proof scheme for p if (1) p, = p, and for every i (2) Q = p % <- q h ... ,q n , ir u ..., -.r m , where {q l ,...,q n } C {pi t ...p i - 1 } and Ui =Ui-i U{r u ...,r m }. We call p the conclusion of 5, written p = cln(S), and the set U, the support of 5, written supp(S). We say that a subset M C H P admits a proof scheme S = ((ft,C il C/ t ))LiifMn[/ s = 0. The following proposition due to Marek, Nerode,and Remmel in [MNR90] characterizes stable models in terms of the existence of proof schemes. Proposition 6.4.93 Let M C H P . Then M is a stable model of P if and only if (1) for every pe M, there is a proof scheme S for p such that M admits S, and (2) for every pi M, there is no proof scheme S for p such that M admits S. As stated in the introduction, restrictions on the number of proof schemes greatly reduce the possible complexity of the set of stable models of a recursive logic program P. But how many derivation schemes for an atom p can there be? If we allow P to be infinite, then it is easy to construct an example with infinitely many derivations of a single atom. Moreover given two proof schemes, one can insert one 117 into the other (increasing appropriately the sets Ui in this process, with obvious restrictions). Thus various clauses C { may be immaterial to the purpose of deriving p. This leads us to introduce a natural relation -< on proof schemes using a well- known device from proof theory. Namely, we define Si -< S 2 if Si , S 2 have the same conclusion and if every clause appearing in Si also appears in S 2 . Then a minimal proof scheme for p is defined to be a proof scheme S for p such that whenever S' is a proof scheme for p and S' -< S, then S -< S'. Note that -< is reflexive and transitive, but -< is not antisymmetric. However it is wellfounded. That is, given any proof scheme S , there is an S' such that S' -< S and for every S", if S" -< S', then S' -< S". Moreover, the associated equivalence relation, S = S', defined by S -< S' and S' -< S, has finite equivalence classes. Example 6.4.32 Let Pi be the following program: C x : p(0)<-^q{Y). C 2 : nat(0) <- . C 3 : nat(s(X)) <- nat{X). Then atom p(0) possesses infinitely many minimal proof schemes. For instance, each one-element sequence Si = ((p(0), Ci0j, {s^O)})) where 6 t is the operation of substituting s l (0) for Y , is a minimal proof scheme for p(0). However if program P 2 is the result of replacing clause C\ by C[: q ( s (Y))^^q(Y), each atom possesses only finitely many minimal proof schemes. We shall call a program P locally finite if for every atom p, there are only finitely many minimal proof schemes with conclusion p. If P is locally finite and p G H P , we let D p denote the union of all supports of minimal proof schemes of p. Clearly for any M C H P , the question of whether p has a P, M-derivation depends only onMflDp. This implies that if P is locally finite, when we attempt to construct 118 a subset M C H P which is a stable model for P, we can apply a straightforward (although still infinite) tree construction to produce such an M, if such an M exists at all. Next, we need to make the notion of a recursive program precise. First, assume that we have a Godel numbering of the elements of the Herbrand base H P . Thus, we can think of each element of the Herbrand base as a natural number. U p € H P , write c(p) for the code or Godel number of p. Let u = {0, 1,2,.. .}. Assume [,] is a fixed recursive pairing function which maps w x uj onto u> which has recursive projection functions *, and 7r 2 , defined by ni([x u x 2 }) = x { for all x 1 and x 2 and i e {1,2}. Code a finite sequence (x u . . . , x n ) for n > 3 by the usual inductive definition [x 1 ,...,x n } = [xi, [x 2 , . . . ,x n }}. Next, code finite subsets of a; via "canonical indices". The canonical index of the empty set, 0, is the number and the canonical index of a nonempty set {x , ..., x n }, where x Q < . . . < x n , is ££_, 2 X * . Let F k denote the finite set whose canonical index is k. Once finite sets and sequences of natural numbers have been coded, we can code more complex objects such as clauses, proof schemes, etc. as follows. Let the code c(C) of a clause C = p <r- q u . . . , q n , -r u -rr m be [c(p), k, I], where k is the canonical index of the finite set {c(ft), . . . , c(q n )}, and I is the canonical index of the finite set {c( ri ), ..., c(r m )}. Similarly, let the code c(S) of a proof scheme S = ({p u Q, f/,))^ be [s, [[c( Pl ), c(d), c{U x )\, . . . , [c(p s ), c(C s ), c(U s )}]}, where for each i, c(Ui) is the canonical index of the finite set of codes of the elements of Ui. The first coordinate of the code of a proof scheme is the length of the proof scheme. Once we have defined the codes of proof schemes then for locally finite programs we can define the code of the set D p consisting of the union of the supports of all minimal proof schemes for P. Finally we code recursive sets as natural numbers. Let <f> , &, . . . be an effective list of all partial recursive functions where <t> e is the partial recursive function computed by the e-th Turing machine. By definition, a (recursive) index of a recursive set R is an e such that <j) e is the characteristic function of R. Call 119 a program P recursive if the set of codes of the Herbrand universe Hp is recursive and the set of codes of the clauses of the program P is recursive. If P is a recursive program, then by an index of P we mean the code of a pair [u, p] where u is an index of the recursive set of all codes of elements in Hp and p is an index of the recursive set of the codes of all clauses in P. For the rest of this disscusion we shall identify an object with its code as described above. This means that we shall think of the Herbrand universe of a program, and the program itself, as subsets of u and clauses, and proof schemes as elements of a;. We also need to define various types of recursive trees and n° classes. Let uo <u be the set of all finite sequences from u> and let 2 <u ' be the set of all finite sequences of O's and l's. Given a = (c*i, . . . , a n ) and (3 - (ft, . . . , k ) in u; <w , write a Q (3 if a is initial segment of ft i.e. , if n < k and ojj = fa for i < n. In this paper, we identify each finite sequence a = (cti, . . . , a n ) with its code c(a) = [n, [c*i, . . . , a n ]] in Uf. Let be the code of the empty sequence 0. When we say that a set S C u <UJ is recursive, recursively enumerable, etc., what we mean is that the set {c(a):a 6 5} is recursive, recursively enumerable, etc. Define a tree T to be a nonempty subset of lu <uj such that T is closed under initial segments. Call a function f:u — > u> an infinite path through T provided that for all n, (/(0), . . . , /(n)> € T. Let [T] be the set of all infinite paths through T. Call a set A of functions a n^-class if there exists a recursive predicate R such that A = {f:u -> u :Vn(R(n, [/(0), . . . , /(n)])}. Call a Til-class A recursively bounded if there exists a recursive function g: u — > u such that V/ G A\fn(f(n) < g(n)). It is not difficult to see that if A is a rij-class, then A = [T] for some recursive tree T C uj <u} . A tree T C uj <u) is highly recursive if T is a recursive finitely branching tree and also there is a recursive procedure which, applied toa= (oi, ... , a n ) in T, produces a canonical index of the set of immediate successors of a in T. Then if C is a recursively bounded flj-class, it is easy to show 120 that C = [T] for some highly recursive tree T C u <UJ , see CR98. For any set A C to, the set A' = {e:<j>^{e) is defined} is called the jump of A, let 0' denote the jump of the empty set 0. We write A <t B if A is Turing reducible to B and A = T B if A < T B and B <t A. A function / : C -» D is said to be degree-preserving if ;4 =r /(4) for all A EC. Even if F is a locally finite program, there is no guarantee that the global be- havior of the function p t-¥ D p , mapping u> into u>, has any sort of effective properties. Thus we are led to define the following. We say that a locally finite recursive program F possesses a recursive proof structure (rps) if (1) F is locally finite, and (2) the function p i-> D p is recursive. A locally finite recursive program with an rps is called an rps program. 6.5 Equivalence of Logic Programming to Nonmonotonic Rule Systems The equivalence of Logic Programming to Nonmonotonic Rule Systems has been shown by Cenzer, Marek, Nerode, Remmel and others. Here, we give the equivalence as shown by Cenzer and Remmel [CR99]. We shall encode now the stable models of logic programs as extensions of suitably chosen nonmonotonic rule systems. The universe of all our systems, U, will be the Herbrand base of the program. Next, to every general propositional clause C, C =p<r- q u ...,q m ,^r u ...,-^r n assign the rule 9i,...,9m :ri,...,r„ re = • P Now, given the program F, define Np = {r c : C 6 ground{P)} We then have the following result 121 Theorem 6.5.94 Let P be a general logic program. Let M be a subset of the tier- brand base of P. Then M is a stable model of P is and only if M is an extension of the nonmonotonic rule system (U,Np). Theorem 6.5.94 allows us to obtain results concerning stable models of logic programs from theorems about extensions of nonmonotonic rule systems. These theorems and other similar results obtained in mnr90a,mnr90b indicate why nonmonotonic rule systems are useful in the investigations of various nonmono- tonic logical formalisms. The results, both positive and, to some extent, negative, on nonmonotonic rule systems provide us with corresponding results for all these formalisms. 6.6 Previous Results Through the Eves of Logic Programming In this section, we shall introduce the key notion of a locally determined logic program P. The informal notion of a locally determined logic program P is one in which the existence of a proof scheme for an atom a, (or the lack of existence thereof) can be determined by examining only clauses or proof schemes involving some initial segment of the Herbrand base of P. More formally, fix some countable logic program P and some listing a Q , Oi, . . . of the atoms of Herbrand base of P without repetitions. (We shall make the convention that if P is recursive logic program, then there is some recursive function h such that h(i) = a { .) Then given a proof scheme or a clause </>, we write max(<f)) for the max({i : a { occurs in 0}). We shall write P n for the set of all clauses C e P such that max(C) < n and let A n = {a , . . . ,o»}. Definition 6.6.95 We shall say that n is a level of P if for all S C {a , . . . ,a„} and all i < n, whenever there exists a proof scheme ip such that cln{i>) = a t and supp(tp)llS = 0, then there exists a proof scheme <p such that cln(4>) = a it supp{(j)) n S = and max(<f>) < n. Note that by definition, the Herbrand base H Pn of P n is contained in A„ 122 Theorem 6.6.96 Suppose that n is a level of P and E is a stable model of P. Then E n = E fl {a , . . . , a n } is a stable model of P n . Proof: If E is a stable model of P, then for any a* G E n , there is a proof scheme ip such that cln(ip) — aj and supp(ip) f) E = 0. Thus, in particular, supp(ip) n E n = so that since n is a level, there exists a proof scheme <j> such that max((j)) < n, cln(<(>) = a,, and supp{(j>) C\E n = $. Thus <£ is a proof scheme of P n and E n admits <f>. Vice versa, if i < n and a* is not in £ n , then there can be no proof scheme <fi of P n such that cln((j)) = a*, max(4>) < n, and supp((j)) fl £„ = since this would violate the fact that E is a stable model of of P. Thus E n is a extension of P n . Definition 6.6.97 1. We shall say that a logic program P is locally determined if P is countable and there are infinitely many n such that n is a level of P. 2. Suppose that P is a recursive logic program. Then we say that P is effectively locally determined if P is locally determined and there is a recursive function f such that for all i, f(i) > i and f(i) is a level of P. Notation: If P is locally determined, we let lev(P) — {n : n is a level of P}. In [MNR90 and MNR92a], Marek, Nerode, and Remmel showed that the problem of finding a stable model of a locally finite recursive logic program can be reduced to finding an infinite path through a finitely branching recursive tree and the problem of finding a stable model of a rsp logic program can be reduced to finding an infinite path through a highly recursive tree. A locally determined logic program is not always locally finite since it is possible that a given atom has infinitely many proof schemes which involves arbitrarily large atoms. Vice versa, it is possible to give examples of locally finite logic programs which are not locally determined. Nevertheless, we shall see that we get similar results to those of Marek, Nerode, and Remmel for locally determined and effectively locally determined recursive logic programs. 123 Theorem 6.6.98 Let P be a recursive logic program. 1. If P is locally determined, then there is a recursive finitely branching tree T and a 1:1 degree preserving correspondence between the set set of stable models £ of P and [T] and 2. If P is effectively locally determined, then there is a highly recursive finitely branching tree T and a 1:1 degree preserving correspondence between the set set of stable models £ of P and [T] . Proof: There is no loss in generality in assuming that H p = u and that a = 0, ai = 1, Next observe that for each n, P n has only finitely many minimal proof schemes so that we can effectively list all minimal proof schemes </> < fa < . . . in such a way that 1. if max((f) k ) = i and max{(j)i) = j and i < j, then k < I. (This says that if i < j, then the proof schemes whose max is i come before those proof schemes whose max is j.) 2. ifmax((j) k ) = max(<t>{) = i, k < I if and only if c(<f> k ) < c{<j>i) where c{4>) denotes the index assigned to a proof scheme <j> under our effective Godel numbering of the proof schemes. We shall encode a stable model M of P by a path * M = (xfc,*!,. . .) through the complete ^-branching tree lj <uj as follows. First, for all i > 0, 7r 2i = xm(0- That is, at the stage 2z we encode the information if i belongs to M. Next, if 7r 2i = then 7T2i+i = 0. But if 7r 2i = 1 so that i 6 M, then 7r 2l+ i = q M {i) where q M (i) is the least q such cln((j) Q ) = i and supp{<j) q ) n M = 0. Thus </> 9mW is the least proof scheme which shows that i € Fp <M . 124 Clearly M < T tt m since it is enough to look at the values of tt m at the even levels to read off M. Now given an M-oracle, it should be clear that for each i £ M, we can use an M-oracle to find 9m(0 effectively. This means that ty m < t M. Thus the correspondence M h-> tx m is an effective degree-preserving correspondence. It is trivially one-to-one. Next we construct a recursive tree T C u u such that [T] = {tte : E is a stable model of P}. Let L k = max({i : max((j)i) < k}). It is easy to see that since P is a locally determined recursive logic program, we can effectively calculate L k from A;. We have to say which finite sequences belong to our tree T. To this end, given a sequence a = (cr(0), . . . , a(k)) € w <UJ set l„ = {i : 2z < k A a(2i) = 1} and O a = {i : 2i < k A a(2i) = 0}. Now we define T by putting a into T if and only if the following four conditions are met: (a) Vi(2? + 1 < k A a(2i) = => a(2i + 1) = 0). (b) Vi(2? + 1 < k A cr(2z) =la> cr(2z + 1) = q where </>, is a minimal proof scheme such that cln(<j) q ) = i and supp(<f) q ) n I a = 0). (c) Vz(2z + 1 < k A cr(2i) = 1 => there is no c € L LJt/2 j such that dn(^ e ) = », supp((j) c ) C CT and c < <r(2i + 1)). (here [-J is the so-called number-theoretic "floor" function). (d) Vi(2i < k A tr(2i) = => there is no c e L Lfc/2 j such that c/n(c/> c ) = i and supp((j) c ) C O ff ). It is immediate that if a G T and r Qa, then r G T. Moreover it is clear from the definition that T is a recursive subset of u <w '. Thus T is a recursive tree. Also, it is easy to see that our definitions ensure that, for any stable E of P, the sequence n B is a branch through T, that is, ir E G [T]. We shall show now that every infinite branch through T is of the form -n E for a suitably chosen stable model E. To this end assume that /3 - (/?(0), /?(!), . . .) is 125 an infinite branch through T. There is only one candidate for E, namely E = {i ; /3(2i) = 1}. Two items have to be checked, namely, (I) E$ is an stable model of P and (II) 7r {Eg) = p. To prove (I), first observe that if i e E , then a(2i) = 1 and o(2i + 1) = q where (j) q is a proof scheme such that cln((j) q ) = i. Moreover condition (c) and the fact that a n = (P , Pi, . . . , p n ) e T for all n > 2% + 1 easily imply that supp((p q ) n I„ n - for all such n and hence supp((j) q ) D Ep = 0. In addition, condition (c) ensures that <?!> g is the least proof scheme with this property. Similarly if i £ Ep, then condition (d) and the fact that a n - {Po,Pi, . . . , P n ) € T for all n > 2i + 1 easily imply that there can be no proof scheme (f> q with cln(<f) q ) = i and supp((j) q ) f\ Ep = %. It then follows from Proposition 6.4.93 that Eg is a stable model of P and that 7r (£y3 ) = The key fact needed to establish the branching properties of T is that for any sequence a € T and any i, either a(2i) = a(2i + 1) = or a(2i) = 1 and a(2i + 1) codes a minimal proof scheme for i. We just note that when a proof scheme tp = a(2i + 1) does not correspond to a path tt e , then there will be some k such that a has no extension in T of length k. This will happen once we either find a smaller code for a proof scheme or we find some u > i in the support of rf> such that all possible extensions r of a have t(2u) = 1. We claim that T is always finitely branching and that if P is effectively locally determined, then T is highly recursive. Clearly the only case of interest is when 2i + 1 < k and a(2i) = 1. In this case we will let a(2i + 1) = c where cln(<j) c ) = i and supp((j) c ) n 7 a = and there is no a < c such that cln((j) a ) = i and supp((f) a ) (1 I a = 0. Now suppose that p is level and i < p. Then by definition, there must be a minimal proof scheme ip such that max(ip) < p, cln(tp) = i, and supp(ip) D I a = 0. Thus tp = (j) q for some q < L p . It follows that c < L p where p is the least level greater than or equal to i. Thus T is always finitely branching. Now if P is effectively locally 126 determined and this is witnessed by the recursive function /, then it will always be the case that c < Lj^) so that T will be highly recursive. Corollary 6.6.99 Suppose that P is a countable locally determined logic program such that there are infinitely many n such that P n has a stable model E n . Then P has a stable model. Proof: Now consider the tree T constructed for P as in Theorem 6.6.98. Here we again can construct our sequence of minimal proof schemes O , 0i, ■ • • recursive in P just as we did in Theorem 6.6.98. However, we can only conclude that T is recursive in P. Nevertheless, we are guaranteed that T is finitely branching which is all we need for our argument. Now fix some level n and consider some m>n such that P m has an extension E m . Then by the exact same argument as in Theorem 6.6.96, E n = E m n {0, . . . , n} will be a stable model of P n . Now consider the node a En = (ct(0), . . . , a(2n + 1)) such that 1. a{2i) = l\fieE n and u(2i) = if i <$. E n , 2. <7(2z + l) = 0if(7(2t) = 0, and 3. cr(2i + 1) = c where c is least number such that max((f> c ) < n, cln{<j) c ) = i, and supp((f) c )r\E n = 0. (Note it follows from our ordering of minimal proof schemes that <j> c is the least proof scheme <f> such that dn{<j>) = i and supp{<f>)C\E n - 0.) It is easy to check that our construction of T ensures that a G T. It follows that T is infinite finitely branching tree and hence T has infinite path -k by Konig's Lemma. Our proof of Theorem 6.6.98 shows that E„ is an stable model of P. We now give two conditions which ensure the existence of recursive stable models. 127 Definition 6.6.100 1. Let P be a locally determined logic program and lev(P) = {Iq < li < . . .} . Then we say say that P has the level extension property if for all k, whenever E k is a stable model of Pi k , there exists a stable model E k+i ofP ik+l such that E k+i n {a , ...,ai k } = E k . 2. A level n of P is a strong level of P if for any levels m < n of P and any stable model E m of P m , if there is no stable model E of P with Er\{a , . . . , a m } = E m , then there is no stable model E n of P n with E n D {a , . . . , a m } = E m . 3. P has effectively strong levels if P has infinitely many strong levels and there is a computable function f such that for each i, i < f(i) and f(i) is a strong level. In general, it is not easy to ensure that a locally determined logic program P has the level extension property. However, there are many natural examples where this condition is satisfied. One way to generate such programs is to consider the following result from recursive combinatorics. Bean [be76] showed that there there exists highly recursive connected graphs which are 3-colorable but not recursively /c-colorable for any k. However Bean also showed that every infinite connected k- colorable highly recursive graph G is recursively 2/c-colorable. Here a graph G = (V, E) is highly recursive if the edge set V is a recursive subset of w, the set of codes of the sets {x, y} G E is recursive, G is locally finite, i.e. the degree of any vertex v e V is finite, and there is an effective procedure which given any vertex v eV produces a code of N(x) = {y £V : {x,y} e E}. A recursive 2/c-coloring of G can be produced as follows. Given any set W C V, let N(W) = {y G V - W : (3x e W)({x,y} e E}. Then given any x 6 V, define an effective increasing sequence of finite sets = A , Ai,Ai,... where Ai = N(x) U {x} and for all k > 1, A k = A k _ x U N{A k _ x ). It is easy to see that there can be no edge from an element of A k to an element of A k+ 2 - Ak+v Since G is A;-colorable, the induced graph determined by A { - A % _ x is 128 fc-colorable for alii > 1. We then defined a recursive 2/c-coloring of G as follows. (Step 1) Find a coloring of A\ using colors {1, ... k}, (Step 2) Find a coloring of A 2 — Ai using colors {k + 1, . . . , 2k}, (Step 3) Find a coloring of A 3 - A - 2 using colors {1, . . . fc}, (Step 4) Find a coloring A± — A 3 using colors {k + 1 2A;}, etc. One can easily write a logic program to implement this procedure and it will naturally be effectively locally finite and have the level extension property. Theorem 6.6.101 1. Suppose that P is an effectively locally determined recursive logic program with the level extension property. Then for every level n and stable model E n of P n , there is a recursive stable model of E of P such that E(l{a ,...,a n } = E n . 2. Suppose that P is a recursive logic program with effectively strong levels. Then for every level n and stable model E n of P n , if there is a stable model E of P with E D {ao, . . . ,a n } = E n , then there is a recursive stable model of E of P such that E n {a , . . . , a n } = E n . Proof: For (1), fix a level n of P and a stable model E n of P. Suppose that / is the function which witnesses the fact P is effectively locally determined. Then let 60,61,62, ■•• be the sequence n,/(n),/(/(n)), . . .. It is easy to see that our level extension property implies that we can effectively construct a sequence of sets E bo ,E bl ,E b2 ,. . . such that (1) E bo = E n , (2) for all j > 0, E bj is a stable model of P b , and (3) for all j > 0, E bj+1 fl {a , . . . , a bj } = E bj . Now consider tree T and the nodes a Eb as constructed in Corollary 6.6.99. It is easy to check that for all i, a Eb G T and that a EbQ C a Ebi E a Eb2 E • • •• It follows that there is a unique path /3 in [T] which extends all a Eb _ and that E = \J i>0 a Eb , is a stable model of P. Moreover E is recursive because to decide if a, 6 E , one need only find k such that b k > j, in which case, a ; e E <=> a, G CT£ 6 . 129 For (2), assume that / is the recursive function which witnesses the fact that P has strong levels and let 6 , h, h, ■ ■ ■ be defined as above. We claim that the property of strong levels once again lets us construct an effective sequence E bo ,E bi ,E b2 ,... such that (1) E bo = E n , (2) for all j > 0, E bj is a stable model of P bj , and (3) for all j > 0, E bj+l n {a Q ,...,a bj } = E bj . That is, suppose that we have constructed E bk such that there exists a stable model S of P such that S D {a , . . . ,a bk } = E bk . Now consider the strong level b k+2 . Our definition of strong level ensures that there must be some stable model F k+2 of P h+2 such that F k+2 D {a , . . . , a bk } = E bk . Then let Eb k+1 = Fk+2 n {°o, • ■ • , a b k+i }- The argument in Theorem 6.6.96 shows that E bk+l is a stable model of P bk+l . Moreover, since b k+2 is a strong level, there must be a stable model 5' of P such that E bk+l = S' D {a , . . . , a bk+1 } since otherwise, there can be no extension F of P bk+2 such that E bk+1 = F n {a , . . . , a bk+1 }. This given, we can then construct our desired recursive stable model E exactly as in (1). We now consider another, more direct approach to producing a recursive stable model. Definition 6.6.102 We say that a recursive logic program P has witnesses with effective delay if there is a recursive function f such that for all n, f(n) > n and whenever there is a set S C {a Q ,...,a n } such that there is a stable model E of P with E fi {a , ...,a n } = Sbut there is no stable model F of U such that F n {ao, . . . , a n , a n+ i} = S, then either (i) there is a proof scheme <f> with max(<f>) < n + 1 such that cln(cj)) = a n+l and supp{(j)) C {a ,...,a n } - S, or (ii) for all sets T included in {a n+2 , . . . ,a /(n) }, there is a proof scheme ip T with max(ip) < f(n) such that supp(xjj T ) C {a , . . . , a /H } - (T U S) and dn{ipr) e {a , . . . , o /(n) } -(Tu5). 130 Note that in case (i), the proof scheme 4> witnesses that we must have a n+1 in any stable model E such that E n {a , . . . ,a n } = S. In case (ii), the proof schemes <j) T show that we can not have a stable model E of P such that E D {a , . • • , a/ (n) } = S U T so that we are again forced to have a„ +1 in any stable model E such that £n{a ,...,a n } = S. Theorem 6.6.103 Suppose that P is a recursive logic program which has witnesses with effective delay and has at least one stable model. Then the lexicographically least stable model E of P is recursive. Proof: We can construct the lexicographically least stable model E of P by induction as follows. Suppose that for any given n we have constructed E n = E n {a , . . . ,a„}. Then E n +\ = E n unless either (i) there is a proof scheme <j) of level n such that supp(<j)) C {a , ...,a n } - E n and cln((j)) = a n+1 or (ii) for all sets T included in {a n+2 , . . . ,a /(n) }, there is a proof scheme ip T with maxifo) < f(n) such that supper) C {a , . . . , a /(n) } - (T U .£„) and cin(^r) 6 {a , . . . , a /{n) } - (TU ^„). in which case £ n+1 = £ n U {a n+1 }. Note that since there are only finitely many minimal proof schemes <j) with max(4>) < k for any given k, we can check conditions (i) and (ii) effectively. Since there is a stable model, it is easy to see that our definitions insure that E n is always contained in the lexicographically least stable model of P. Thus E = \J n E n is recursive. By putting suitable effective bounds on the effective levels and/or the witnesses with effective delay, one can readily come up with conditions that force P to have exponential time, NP, or P-time stable models. CHAPTER 7 FUTURE DIRECTIONS There are many avenues of research yet to be explored in Nonmonotonic Rule Systems and other forms of Nonmonotonic Logic, including Default Logic and Logic Programming. As far as common derivations are concerned, we have only scratched the surface. There are three extensions of the research which should be followed, namely further work in the complexity of the common derivation, applications of the current results, and combining Nonmonotonic Rule Systems with Fuzzy Logic and/or Multiple- Valued Logic. The complexity of the common derivations have been touched upon in this dissertation, but have been by no means exhaustively studied. In addition, we might consider a multitude of other types of complexity aside from those mentioned here. Some of the original motivation for the results in this dissertation was to create the mathematics necessary to apply Nonmonotonic Logic to such areas as advertising, political campaigning, and other social sciences. The results, at this point, I believe are sufficient to begin the creation of models for use in these fields. As a matter of practicality, these models should be included in the future directions of this research. To combine Nonmonotonic Rule Systems with Fuzzy Logic and/or Multiple- Valued Logic may seem a strange or unrelated road to follow from the present work. However, Nonmonotonic Logic was initially established with the intention of formal- izing human reasoning. It is optimistic in the least to suppose that every human belief and thought carries a black-and-white value of true or false. Human reason- ing often treads a grey area somewhere in between. Thus, Fuzzy Logic or at least Multiple- Valued logic is called for. In Nonmonotonic Rule Systems we may use any 131 132 underlying logical system to govern U. Interesting results may first be found in the comparitively less complicated world of Multiple- Valued Logic, begining with three values and generalizing results to n-valued logic. From there, choosing Fuzzy Logic to be the "logic of choice" for the Nonmonotonic Rule System < U,N > would be the natural step to take. This is by no means a complete list of possible future directions. Nonmono- tonic Logic, a vigorous and rapidly growing area of research, is still in its infancy. There are many questions still to be answered, and each new result brings its weight in new roads to follow. REFERENCES [AN78] H. Andreka, and I. Nemeti. The Generalized completeness of horn predi- cate logic as a programming language. Acta Cybernetica 4(1978): 3-10. [Apt90] K.R. Apt. Logic programming. Handbook of theoretical computer science, J. van Leeuven, (ed.). Cambridge, MA: MIT Press, 1990. [AB90] K.R. Apt, and H.A. Blair. Arithmetical classification of perfect models of stratified programs. Fundamenta Informaticae 13 (1990): 1-17. [B90] J. Banks. A model of electoral competition with incomplete information. Journal of Economic Theory 50 (1990): 309-325. [Be76] D.R. Bean. Effective coloration. Journal of Symbolic Logic 41 (1976): 469- 480. [BDK97] G. Brewka, J. Dix, and K. Konolige. Nonmonotonic reasoning: An overview. Stanford, CA: CSLI, 1997. [BG97] G. Brewka, and G. Gottlob. 1997. Well-founded semantics for default logic. Fundamenta Informaticae 31(3-4) (1997): 221-236. [CMMT95] P. Cholewihski, W. Marek, A. Mikitiuk, and M. Trusczcyhski. Exper- imenting with nonmonotonic reasoning. Proceedings of the Twelfth In- ternational Conference on Logic Programming 267-281. Cambridge, MA: MIT Press, 1995. [CMT96] P. Cholewihski, W. Marek, and M. Trusczcyhski. Default reasoning sys- tem DeRes. Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning, L. Carlucci Aiello, J. Doyle and S. Shapiro (eds.). KR96 (1996): 518-528. [CR98] D. Cenzer and J.B. Remmel. ITj'-classes in mathematics. Handbook of recursive mathematics: Volume 2, Yu. L. Ershov, S.S. Goncharov, A. Nerode, and J.B. Remmel (eds.). Studies in Logic and the Foundations of Mathematics, 139: 623-822. Amsterdam: Elsevier, 1998. [CR99] D. Cenzer, and J. Remmel. Complexity, decidability, and completness. Preprint. [CRV99] D. Cenzer, J.B. Remmel, and A.K.C.S. Vanderbilt. Locally determined logic programs. Proceedings of the 5th international Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR99). Berlin: Springer- Verlag, 34-49. 1999. [Do79] J. Doyle A truth maintenance system. Artificial Intelligence 12 (1979): 231-272. 133 134 [DM82] J. Doyle and D. McDermott. Nonmonotonic logic II: nonmonotonic modal theories. Journal of the A.C.M. 29 (1982): 33-57. [EG93] T. Eiter, and G. Gottlob. Complexity results for disjunctive logic pro- gramming and application to nonmonotonic logics. Proceedings of the Tenth International Logic Programming Symposium (ILPS-93). Cam- bridge, MA: MIT Press, 1993, 266-278. " [EMTT96] J. Engelfriet, W. Marek, J. Treur, and M. Truszczyriski. Infmitary de- fault logic for specification of nonmonotonic reasoning. Logics in Artificial Intelligence, Proceedings European Workshop on Logics in Artificial In- telligence, JELIA'96. Lecture notes in Artificial Intelligence 1126 (1996): 224-236. [GL88] M. Gelfond and V. Lifschitz. The stable semantics for logic programs. Proceedings of the 5th International Symposium on Logic Programming. Cambridge, MA: MIT Press, 1988, 1070-1080. [Gol94] C. Goldburg. The accuracy of game theory predictions for political be- havior: cumulative voting in illinois revisited. Journal of Politics 56(4) (1994): 885-900. [Got92] G. Gottlob. Complexity results for nonmonotonic logics. Journal of Logic and Computation 2(3) (1992): 397-425. [Got93] G. Gottlob. Recent complexity results in logic programming and non- monotonic reasoning and why they matter. Proceedings of the Second International Workshop on Logic Programming and Nonmonotonic Rea- soning LPNMR'93. Cambridge, MA: MIT Press, 1993, 265. [Got95] G. Gottlob. The complexity of default reasoning under the stationary fixed point semantics. Information and Computation 121(1) (1995): 81- - * _ . [GM94] G. Gottlob, and Z. Mingyi. Cumulative default logic: finite characteriza- tion, algorithims and complexity. Artificial Intelligence 69 (1994): 329- [MNR90] W. Marek, A. Nerode, and J. Remmel. A theory of nonmonotonic rule systems I. Annals of Mathematics and Artificial Intelliqence 1 (1990): 241-273. [MNR92a] W. Marek, A. Nerode, and J. Remmel. A theory of nonmonotonic rule systems II. Annals of Mathematics and Artificial Intelliqence 51 (1992): 229-263. [MNR92b] W. Marek, A. Nerode, and J. Remmel. How complicated is the set of stabile models of a recursive logic program? Annals of Mathematics and Artificial Intelligence 56 (1992): 119-135. [MNR92c] W. Marek, A. Nerode, J. Remmel. The stable models of a predicate logic program. Journal of Logic Programming 21(3) (1992): 129-154. [MNR94] W. Marek, A. Nerode, and J. Remmel. A context for belief revision: forward chaining-normal nonmonotonic rule systems. Annals of Pure and Applied Logic 67(1-3) (1994): 269-323. 135 [MNR94a] W. Marek, A. Nerode, and J. B. Remmel. The stable models of predicate logic programs. Journal of Logic Programming 21 (1994): 129-154. [MNR95] W. Marek, A. Nerode, and J. Remmel. Complexity of normal default logic and related modes of nonmonotonic reasoning. Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science Cambridge, MA: MIT Press (1995): 178-187. [MNR97a] W. Marek, A. Nerode, and J. Remmel. Complexity of recursive normal default logic. Fundamenta Informaticae 32(2) (1997): 139-148. [MNR97b] W. Marek, A. Nerode, and J. Remmel. Nonmonotonic rule systems with recursive sets of restraints. Archivfur Mathematische Logik36 (1997): 339-384. [MNR99a] W. Marek, A. Nerode, and J. Remmel. Logic programs, well-orderings and forward chaining. Annals of Pure and Applied Logic 96 (1999): 231- 276. [MNR99b] W. Marek, A. Nerode, and J. Remmel. Forward chaining-normal non- monotonic rule systems. Preprint. 1999. [MS89] W. Marek, and V. S. Subrahmanian. Relationship between logic program semantics and nonmonotonic reasoning. Proceedings of the Sixth Inter- national Conference on Logic Programming. Cambridge, MA: MIT Press (1989), 417-419. [MST91] W. Marek, G. Schwartz, and M. Truszczyhski. Ranges of strong nonmono- tonic logics. Nonmonotonic Logic and Inductive Logic. Springer Lecture Notes in Computer Science 543 (1991): 85-99. [MT89a] W. Marek and M. Truszczyhski. Stable semantics for logic programs and default theories. Proceedings of North American Conference on Logic Programming. Cambridge, MA: MIT Press (1989), 243-256. [MT89b] W. Marek and M. Truszczyhski. Relating autoepistemic and default log- ics. Proceedings of the International Conference on Knowledge Represen- tation KR89, San Fransisco, CA: Morgan-Kaufman (1989), 276-288. [MT90] W. Marek and M. Truszczyhski. Modal logic for default reasoning. Annals of Mathematics and Artificial Intelligence 1 (1990): 275-302. [MT92] W. Marek and M. Truszczyhski. More on modal aspects of default logic. Fundamenta Informaticae 17(1-2) (1992): 99-116. [MT93a] W. Marek and M. Truszczyhski. Nonmonotonic logics; context-dependent reasoning. Berlin: Springer- Verlag, 1993. [MT93b] W. Marek and M. Truszczyhski. Normal form results for default logic, nonmonotonic and inductive logic II. Springer Lecture Notes in Computer Science, G. Brewka, K. P. Jandtke, and P. H. Schmitt (eds.), 659 (1993): 270-283. [MTT97] W. Marek, J. Treur, and M. Truszczyhski. Representation theory for default logic. Annals of Mathematics and Artificial Intelligence 21 (1997): 343-358. 136 [MZ90] W. Marek, and A. Zhang. On the classification and existence of structures in default logic. Fundamenta Informaticae 13(4) (1990): 485-499. [Rei80] R. Reiter. A logic for default reasoning. Artificial Intelligence, 13 (1980): 81-132. BIOGRAPHICAL SKETCH Amy K. C. S. Vanderbilt was born Amy Kathryn Colleen Sartain on February 17, 1975, in Fayetteville, Tennessee. She moved to Orlando, Florida, in 1978 where she lived until 1992 and attended Lake Highland Preparatory School. In 1992 she moved to Gainesville, Florida, to attend the Univeristy of Florida earning a bachelor's degree in mathematics in 1995, a master's degree in pure mathematics in 1997 and a doctorate in mathematics, specializing in logic, in May of 2000. 137 I certify that I have read this study and that in my opinion it conforms to acceptable standards of scholarly presentation and is fully adequate, in scope and quality, as a dissertation for the degree of Doctor of Philosophy. ^1_£ j£ ?*g£4L Douglas A. Cenzer, Chairman Professor of Mathematics I certify that I have read this study and that in my opinion it conforms to acceptable standards of scholarly presentation and is fully adequate, in scope and quality, as a dissertation for the degree of Doctor of Philosophy. ■^7^. [A' <7"^-C^-<r*-^ Jean A. Larson Professor of Mathematics I certify that I have read this study and that in my opinion it conforms to acceptable standards of scholarly presentation and is fully adequate, in scope and quality, as a dissertation for the degree of Doctor of Philosophy. -tK^L Rick L. Smith Associate Professor of Mathematics I certify that I have read this study and that in my opinion it conforms to acceptable standards of scholarly presentation and is fully adequate, in scope and quality, as a dissertation for the degree of Doctor of Philosophy. O Jorge Martinez Professor of Mathematics I certify that I have read this study and that in my opinion it conforms to acceptable standards of scholarly presentation and is fully adequate, in scope and quality, as a dissertation for the degree of Doctor of Philosophy. Beverly A. Sanders Associate Professor of Computer and Information Science and Engineerng This dissertation was submitted to the Graduate Faculty of the Department of Mathematics in the College of Liberal Arts and Sciences and to the Graduate School and was accepted as partial fulfillment of the requirements for the degree of Doctor of Philosophy. May 2000 Dean, Graduate School LD - . 1 20 CL t \lW UNIVERSITY OF FLORIDA 3 1262 08555 3393